{X} {a b c : X} {p : a = b} {q : b = c} {r} (theta : p @ q = r) : (lrucancel 1 [I] lrucancel 1) @ whiskerR theta _ = whiskerL _ theta @ (lrucancel 1). Proof. by destruct theta, p, q. Defined.
From HoTT Require Import Basics Types.