diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/JMeq.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index a44edfbf27..47a20a63d9 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -14,34 +14,35 @@ Set Implicit Arguments. Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := JMeq_refl : (JMeq x x). +Reset JMeq_ind. Hints Resolve JMeq_refl. -Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). +Lemma sym_JMeq : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). NewDestruct 1; Trivial. Qed. -Hints Immediate JMeq_sym. +Hints Immediate sym_JMeq. -Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C) +Lemma trans_JMeq : (A,B,C:Set)(x:A)(y:B)(z:C) (JMeq x y)->(JMeq y z)->(JMeq x z). NewDestruct 1; Trivial. Qed. Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y). -Lemma JMeq_eq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y). +Lemma JMeq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y). Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial. Qed. -Lemma JMeq_eq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y). +Lemma JMeq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y). Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial. Qed. -Lemma JMeq_eq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x). -Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial. +Lemma JMeq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x). +Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial. Qed. -Lemma JMeq_eq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x). -Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial. +Lemma JMeq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x). +Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial. Qed. |