proposition: Theorem eh {X} {a : X} (p q : idpath a = idpath a) : p @ q = q @ p.
proof: Proof. refine (_ @ rlucancel_inv (urnat q [-] ulnat p)). refine ((rlucancel_inv (ulnat p [-] urnat q))^ @ _). exact (wlrnat p q). Defined.
imports: HoTT(Basics Types)