Fixpoint helper_C m n : m = n -> nat_discern m n. Proof. intros e. destruct e. exact (cast (! nat_discern_unit m) tt). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.