{A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) {z : A} (s : y = z) : (ap f q) @ (p y @ s) = (p x) @ (q @ s). Proof. destruct q, s; cbn. apply concat_1p. Defined.
Require Import Basics.Overture Basics.Tactics.