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