{A} {x : A} (h : idpath x = idpath x) : whiskerR h 1 = h. Proof. refine (_ @ whiskerR_p1 h); simpl. symmetry; refine (concat_p1 _ @ concat_1p _). Defined.
Require Import Basics.Overture Basics.Tactics.