proposition: Lemma subtree_wf : wf subtree.
proof: Proof. Proof using. intros t. induction t using tree_induct_mem; constructor; introv K; inversions~ K. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)