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