Representing trees with functions

Consider the following inductive type for binary trees (with nodes labeled by integers). 
Require Import ZArith.

Inductive Z_fbtree : Set :=
 | Z_fleaf : Z_fbtree 
 | Z_fnode : Z  -> (bool -> Z_fbtree) -> Z_fbtree.
Define a function fzero_present:Z_fbtree -> bool that maps any tree t to true if and only if t contains the value zero.

Solution

This file