Lemma mt_path_refl (T:Tree) (x y:T) : x = y -> mt_dist _ x y = 0. Proof. intros e. destruct e. apply mt_refl. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Nat. Import UniMath.MoreFoundations.Nat.Discern. Require Import UniMath.MoreFoundations.Notations.