fact: Definition concat_whisker {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') : (whiskerR a q) @ (whiskerL p' b) = (whiskerL p b) @ (whiskerR a q') := match b with idpath => match a with idpath => (concat_1p _)^ end end.
imports: Basics.Overture Basics.Tactics