We define a type of trees based on lists of trees. In this type, an node can have an arbitrary (but finite) number of children, grouped in a list.
Inductive ltree (A:Set) : Set := lnode : A -> list (ltree A)-> ltree A.
For this type, the induction principles that are generated by default or by the Scheme command are un suitable, but we can construct a suitable with the following script.
Section correct_ltree_ind. Variables (A : Set)(P : ltree A -> Prop)(Q : list (ltree A)-> Prop). Hypotheses (H : forall (a:A)(l:list (ltree A)), Q l -> P (lnode A a l)) (H0 : Q nil) (H1 : forall t:ltree A, P t -> forall l:list (ltree A), Q l -> Q (cons t l)). Fixpoint ltree_ind2 (t:ltree A) : P t := match t as x return P x with | lnode a l => H a l (((fix l_ind (l':list (ltree A)) : Q l' := match l' as x return Q x with | nil => H0 | cons t1 tl => H1 t1 (ltree_ind2 t1) tl (l_ind tl) end)) l) end. End correct_ltree_ind.
Prove a suitable induction principle for lists of trees of type ltree A.