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