fact: Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) : (ap f q) @ (p y) = (p x) @ q := match q with | idpath => concat_1p_p1 _ end.
imports: Basics.Overture Basics.Tactics