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