proposition: Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x').
proof: Proof. intros. split with (isProofIrrelevantUnit x x'). intros e'. induction x. induction x'. simpl. apply unitl3. Defined.
imports: UniMath.Foundations.Preamble