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.
Require Export List. Inductive ltree (A:Set) : Set := lnode : A -> list (ltree A)-> ltree A.
We can define a similar type using mutual inductive types as in the following definition:
Inductive ntree (A:Set) : Set := nnode : A -> nforest A -> ntree A with nforest (A:Set) : Set := nnil : nforest A | ncons : ntree A -> nforest A -> nforest A.
Define functions ltree_to_ntree and ntree_to_ltree that establish a bijection between the two types and prove the bijection property.