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