Lemma unitl3: ∏ e : tt = tt, e = idpath tt. Proof. intros. assert (e0 : unitl0 (idpath tt) = unitl0 e). { apply coconustot_isProofIrrelevant. } set (e1 := maponpaths unitl1 e0). apply (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))). Defined.