Lemma linv_eq_rinv (x lx rx : X) (lxlinv : islinvel x lx) (rxrinv : isrinvel x rx) : lx = rx. Proof. intros. refine (!runax_is is _ @ _). refine (!maponpaths (λ z, lx * z) rxrinv @ _). refine (!assocax_is is _ _ _ @ _). refine (maponpaths (λ z, z * rx) lxlinv @ _). apply lunax_is. Defined.