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 :

Solution

Follow this link