fact: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA