Fixpoint nat_discern (m n:nat) : UU := match m , n with | S m, S n => nat_discern m n | 0, S n => empty | S m, 0 => empty | 0, 0 => unit end. Goal ∏ m n, nat_discern m n -> nat_discern (S m) (S n). Proof. intros ? ? e. exact e. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.