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