We use the type of infinitely branching tree defined as:
Inductive Z_inf_branch_tree : Set := Z_inf_leaf : Z_inf_branch_tree | Z_inf_node : Z->(nat->Z_inf_branch_tree)->Z_inf_branch_tree.We say that a value v is accessible by indices lower than n in a tree t if the tree the tree has the form Z_inf_node v' f and v=v', or if it is (recursively) accessible by indices lower than n in one of the tree f p for p <= n.
Write a function that computes whether the value 0 is accessible by indices lower than a natural number in an infinitely branching tree.