`{P : A -> Type} (f g h : forall x, P x) (p : f == g) (q : g == h) : path_forall f h (fun x => p x @ q x) = path_forall f g p @ path_forall g h q. Proof. revert p q. equiv_intro (@apD10 A P f g) p. equiv_intro (@apD10 A P g h) q. transitivity (path_forall f h (apD10 (p @ q))). - apply ap, path_forall; intros x. symmetry; apply apD10_pp. - refine (eta_path_forall _ _ _ @ _). apply concat2; symmetry; apply eta_path_forall. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids