Lemma tree_deceq (T:Tree) : isdeceq T. Proof. intros. intros t u. induction (isdeceqnat (mt_dist T t u) 0) as [a|b]. { apply inl. apply mt_anti. assumption. } { apply inr. intro e. apply b. 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.