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