proposition: Lemma nat_discern_iscontr m : iscontr (nat_discern m m).
proof: Proof. apply iscontraprop1. { apply nat_discern_isaprop. } { induction m as [|m IHm]. { exact tt. } { simpl. exact IHm. } } Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA