{A B C} (e : B <~> A) (f : B <~> C) (g : A <~> C) : g = f oE e^-1 -> g oE e = f. Proof. intro h. refine (ap (fun g => g oE e) h @ ecompose_eV_e _ _). Defined.
Require Import Basics.Overture Basics.Equivalences Types.Equiv.