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