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