diff options
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 12b0601..bd58e01 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -409,7 +409,7 @@ Lemma bij_eq : bijective f -> forall x y, (f x == f y) = (x == y). Proof. by move/bij_inj; apply: inj_eq. Qed. Lemma can2_eq : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y). -Proof. by move=> fK gK x y; rewrite -{1}[y]gK; apply: can_eq. Qed. +Proof. by move=> fK gK x y; rewrite -[y in LHS]gK; apply: can_eq. Qed. Lemma inj_in_eq : {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}. |