diff options
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6a98af39aa..3e71a60fa6 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail. Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. - intros; intro. + intros A ? x y z H H0 H1. assert(z == y) by (symmetry ; auto). assert(x == y) by (transitivity z ; eauto). contradiction. @@ -95,7 +95,7 @@ Qed. Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. - intros; intro. + intros A ? x y z **; intro. assert(y == x) by (symmetry ; auto). assert(y == z) by (transitivity x ; eauto). contradiction. |