proposition: Lemma tree_induct_mem : forall (P : tree -> Prop), (forall n : nat, P (leaf n)) -> (forall ts : list tree, (forall t, mem t ts -> P t) -> P (node ts)) -> forall t : tree, P t.
proof: Proof. Proof using. introv Hl Hn. eapply tree_induct_gen with (Q := fun ts => forall t, mem t ts -> P t); intros. auto. auto. inverts H. inverts~ H1. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)