Inductive Tree : Set :=
| Leaf
| Node : Tree -> Tree -> Tree.
Inductive Tree7 : Set :=
| T7 : Tree -> Tree -> Tree -> Tree ->
Tree -> Tree -> Tree -> Tree7.
Definition f (ts : Tree7) : Tree :=
match ts with
| T7 Leaf Leaf Leaf Leaf Leaf Leaf (Node t1 t2) =>
match t1, t2 with
| Node s1 s2, Node s3 s4 =>
Node s1 (Node s2 (Node s3 (Node s4 Leaf)))
| Node s1 s2, Leaf =>
Node Leaf (Node Leaf (Node Leaf (Node Leaf (Node Leaf (Node Leaf (Node s1 s2))))))
| Leaf, Node s1 (Node s2 (Node s3 (Node s4 s5))) =>
Node s1 (Node s2 (Node s3 (Node s4 (Node s5 Leaf))))
| Leaf, s1 =>
s1
end
| T7 t1 t2 t3 t4 t5 t6 t7 =>
Node t1 (Node t2 (Node t3 (Node t4 (Node t5 (Node t6 t7)))))
end.
Definition g (t : Tree) : Tree7 :=
match t with
| Node Leaf (Node Leaf (Node Leaf (Node Leaf (Node Leaf (Node Leaf (Node s1 s2)))))) =>
T7 Leaf Leaf Leaf Leaf Leaf Leaf (Node (Node s1 s2) Leaf)
| Node t1 (Node t2 (Node t3 (Node t4 (Node t5 (Node t6 t7))))) =>
T7 t1 t2 t3 t4 t5 t6 t7
| Node s1 (Node s2 (Node s3 (Node s4 (Node s5 Leaf)))) =>
T7 Leaf Leaf Leaf Leaf Leaf Leaf (Node Leaf (Node s1 (Node s2 (Node s3 (Node s4 s5)))))
| Node s1 (Node s2 (Node s3 (Node s4 Leaf))) =>
T7 Leaf Leaf Leaf Leaf Leaf Leaf (Node (Node s1 s2) (Node s3 s4))
| s1 =>
T7 Leaf Leaf Leaf Leaf Leaf Leaf (Node Leaf s1)
end.
