fact: Definition whiskerL_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) : (concat_1p p) ^ @ whiskerL 1 h @ concat_1p q = h := match h with idpath => match p with idpath => 1 end end.
imports: Basics.Overture Basics.Tactics