diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/JMeq.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 127be1134..83edf434e 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -80,9 +80,9 @@ intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial. Qed. Lemma JMeq_congr : - forall (A B:Type) (f:A->B) (x y:A), JMeq x y -> JMeq (f x) (f y). + forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y. Proof. -intros A B f x y H; case JMeq_eq with (1 := H); trivial. +intros A x B f y H; case JMeq_eq with (1 := H); trivial. Qed. (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *) |