The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Yes, the only trick is to use a dependent elimination for type 
DefProp which is not define automatically but can be 
introduced using the Scheme macro :

Scheme DefProp_elim := Induction for DefProp Sort Prop.

Lemma eq_comb
   : (d1,d1':Def1)d1=d1'->(d2:(DefProp d1); d2':(DefProp d1'))
     (c3 d1 d2)=(c3 d1' d2').
Destruct 1.
Intro d2.
Elim d2 using DefProp_elim.
Intros d d2'.
Elim d2' using DefProp_elim; Trivial.
Save.


Nadeem Abdul Hamid writes:
 > Can the following lemma be proven in Coq?:
 > 
 > Inductive Def1 : Set
 >    := c1 : Def1.
 > 
 > Inductive DefProp : Def1 -> Prop
 >    := c2 : (d:Def1)(DefProp d).
 > 
 > Inductive Comb : Set
 >    := c3 : (d:Def1)(DefProp d) -> Comb.
 > 
 > Lemma eq_comb
 >    : (d1,d1':Def1; d2:(DefProp d1); d2':(DefProp d1'))
 >      d1=d1' ->
 >      (c3 d1 d2)=(c3 d1' d2').
 > 
 > Thanks in advance,
 > --- nadeem

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84