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