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