{f : A -> A -> B} `{!Commutative f} `{forall z, StrongExtensionality (f z)} : StrongBinaryExtensionality f. Proof. apply @strong_binary_setoid_morphism_both_coordinates;try apply _. intros z x y. rewrite !(commutativity _ z). apply (strong_extensionality (f z)). Qed.
Require Import HoTT.Classes.interfaces.abstract_algebra.