proposition: Lemma tree_induct : forall (P : tree -> Prop), (forall n : nat, P (leaf n)) -> (forall l : list tree, (forall t, Mem t l -> P t) -> P (node l)) -> forall T : tree, P T.
proof: Proof. Proof using. introv Hl Hn. eapply tree_induct_gen with (Q := fun l => forall t, Mem t l -> P t); intros. auto. auto. inversions H. inversions~ H1. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat