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