Looking for a value in a tree  
Consider the following type:
Require Import ZArith.
Inductive Z_btree : Set :=
 | Z_leaf : Z_btree 
 | Z_bnode : Z->Z_btree->Z_btree->Z_btree.
Define a function taking as argument an integer z 
and a tree t:Z_btree and returning true iff t
has (at least) an occurrence of z.
Hint
Use the function Zeq_bool to compare two intergers wrt equality.
formula.
Solution
 This file 
 Note:  this solution contains also an infix notation
for these formulae.
Suggestion: add propositional variables !