# A counting function for trees and lists of trees.

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.

## Solution

Look at this file

Going home

Pierre Castéran