{A B C} (e : A <~> B) (f : C <~> B) : e oE (e^-1 oE f) = f. Proof. apply path_equiv; apply path_forall; intro; simpl; apply eisretr. Defined.
Require Import Basics.Overture Basics.Equivalences Types.Equiv.