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