The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

Hello everyone.

I have a serious problem with "eq_rect". Here is an example of what I want
to prove. Unfortunately, my proof contains numerous equalities of that kind. 

Lemma test i   n (el:list Expr_IL) l t u w db H :
eq_rect (nth i (repeat_list st_iota n) ds) SDom
        (sem_il (nth_typ i l (refl_equal (length el)) t) u w) st_iota
       H db = 
sem_il (eq_rect (nth i (repeat_list st_iota n) ds)
                 (fun s => typExpr_IL pi (nth i el dE) s)
                 (nth_typ i l (refl_equal (length el)) t) st_iota
                 H)
        u w db.
Proof.
  intros .
  pattern H.
  rewrite H.

These give me the error:

Abstracting over the term "nth i (repeat_list st_iota n) ds"
leads to a term which is ill-typed.

Is there a way to prove such equalities, where dependent types are painful?

Thanks in advance. 


-----
Never say never.
-- 
View this message in context: 
http://www.nabble.com/Problem-with-eq_rect-tp25062341p25062341.html
Sent from the Coq mailing list archive at Nabble.com.