proposition: Lemma nat_discern_inj m n : nat_discern (S m) (S n) -> nat_discern m n.
proof: Proof. intros e. induction m. { induction n. { exact tt. } { simpl in e. exact (fromempty e). } } { induction n. { simpl in e. exact (fromempty e). } { simpl in e. exact e. } } Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA