{X} {a : X} (p q : idpath a = idpath a) : p @ q = q @ p. Proof. refine (_ @ rlucancel_inv (urnat q [-] ulnat p)). refine ((rlucancel_inv (ulnat p [-] urnat q))^ @ _). exact (wlrnat p q). Defined.
From HoTT Require Import Basics Types.