Weaken surjective_homomorphism_from_group

We shouldn't be talking about leibniz equality in groups

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 0c27395f8..5239aae33 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -313,7 +313,7 @@ Module Group.
           {Proper_op:Proper(eq==>eq==>eq)op}
           {Proper_inv:Proper(eq==>eq)inv}
           {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph}
-          {surj:forall h, phi (iph h) = h}
+          {surj:forall h, eq (phi (iph h)) h}
           {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
           {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
           {phi_id : eq (phi ID) id}