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