Lemma nat_discern_inj m n : nat_discern (S m) (S n) -> nat_discern m n. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.