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