`{!IsApart A} `{!IsApart B} `{!IsApart C} {f : A -> B -> C} `{forall z, StrongExtensionality (f z)} `{forall z, StrongExtensionality (fun x => f x z)} : StrongBinaryExtensionality f. Proof. intros x₁ y₁ x₂ y₂ E. apply (merely_destruct (cotransitive E (f x₂ y₁))). intros [?|?];apply tr. - left. apply (strong_extensionality (fun x => f x y₁));trivial. - right. apply (strong_extensionality (f x₂));trivial. Qed.
Require Import HoTT.Classes.interfaces.abstract_algebra.