proposition: Lemma nat_discern_unit m : nat_discern m m = unit.
proof: Proof. induction m as [|m IHm]. { reflexivity. } { simpl. apply IHm. } Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA