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