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