Definition Tree : Type := ∑ (mt_set: Type) (mt_dist: mt_set -> mt_set -> nat) (mt_refl: ∏ x, mt_dist x x = 0) (mt_anti: ∏ x y, mt_dist x y = 0 -> x = y) (mt_symm: ∏ x y, mt_dist x y = mt_dist y x) (mt_trans: ∏ x y z, mt_dist x z <= mt_dist x y + mt_dist y z), ∏ x z, x != z -> ∑ y, (S (mt_dist x y) = mt_dist x z) × (mt_dist y z = 1).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Nat. Import UniMath.MoreFoundations.Nat.Discern. Require Import UniMath.MoreFoundations.Notations.