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