Fixpoint helper_B m n : nat_discern m n -> m = n. Proof. destruct m as [|m']. { destruct n as [|n']. { intros _. reflexivity. } { simpl. exact fromempty. } } { destruct n as [|n']. { simpl. exact fromempty. } { simpl. intro i. assert(b := helper_B _ _ i); clear i. destruct b. reflexivity. } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.