proposition: Lemma coconustot_isProofIrrelevant {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2.
proof: Proof. intros. induction c1 as [x0 x]. induction x. induction c2 as [x1 y]. induction y. apply idpath. Defined.
imports: UniMath.Foundations.Preamble