Need to use Coq functional programming language to solve below question:

Problem 5 (22 points). General Trees:

(a) Define the polymorphic inductive type tree X for trees with arbitrary number of subtrees in each

node. (4 points)

(b) Define mytree of type tree nat depicted in Figure 1. (3 points)

(c) Define a polymorphic function isleaf that checks whether a general tree is a leaf. (4 points)

(d) As a unit test, show that mytree is not a leaf. (1 points)

(e) Define a polymorphic function height that computes the height of general trees. (4 points) Hint:

You may need to define mutually recursive functions using let expressions.

(f) As a unit test, show that the height of mytree is 3. (1 points)

(g) Define a monomorphic function sum_nodes that returns the summation of values within all nodes

of a general tree of type tree nat. (4 points) Hint: You may need to define mutually recursive

functions using let expressions.

(h) As a unit test, show that sum_nodes of mytree is 30. (1 points)

1 5 8 7 3 2 4 Figure 1: mytree