fact: Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) {w z : A} (r : w = f x) (s : y = z) : (r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s).
imports: Basics.Overture Basics.Tactics