Potentially infinite trees

Consider the following definition :

Set Implicit Arguments.

(* potentialy infinite trees with internal nodes labeled with type A *)

CoInductive LTree (A : Set) : Set :=
   LLeaf :  LTree A
 | LBin : A -> (LTree A) -> (LTree A) -> LTree A.

Define the following predicates and functions :

(is_LLeaf t) is a proposition meaning "t is a leaf".
(L_root t) returns the label of the root of t (if exists)
(L_left_son t) returns the left son of t (if exists)
(L_right_son t) returns the right son of t (if exists)
(L_subtree p t) returns the subtree of t at path p (if exists)
(LTree_label p t) returns the label at path p (if exists)

Solution

Follow this link