Definition nat_dist_anti m n : nat_dist m n = 0 -> m = n. Proof. intros i. exact (helper_B _ _ (helper_A _ _ i)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.