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 !


Going home
Pierre Castéran