Corollary tree_isaset (T:Tree) : isaset T. Proof. intros. apply isasetifdeceq. apply tree_deceq. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Nat. Import UniMath.MoreFoundations.Nat.Discern. Require Import UniMath.MoreFoundations.Notations.