diff options
Diffstat (limited to 'theories/Logic/JMeq.v')
| -rw-r--r-- | theories/Logic/JMeq.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 7d9e11296..127be1134 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -43,13 +43,13 @@ Qed. Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. -Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), +Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y, JMeq x y -> P y. Proof. intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. Qed. -Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set), +Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set), P x -> forall y, JMeq x y -> P y. Proof. intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. @@ -61,7 +61,7 @@ Proof. intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. Qed. -Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), +Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y, JMeq y x -> P y. Proof. intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. |