{A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) {w z : B} (r : w = f x) (s : g y = z) : (r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s). Proof. destruct q, s; simpl. induction (p x). reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.