proposition: Lemma tree_deceq (T:Tree) : isdeceq T.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Notations