(f : A -> B -> C) : StrongBinaryExtensionality f. Proof. intros x1 y1 x2 y2 hap. apply (merely_destruct (cotransitive hap (f x2 y1)));intros [h|h];apply tr. - left. apply trivial_apart. intros e. apply tight_apart in h;auto. exact (ap (fun x => f x y1) e). - right. apply trivial_apart. intros e. apply tight_apart in h;auto. Qed.
Require Import HoTT.Classes.interfaces.abstract_algebra.