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