Changing inductive definitions
In searchtrees.v , the predicates
min and maj are inductively defined with the help
of the predicate occ.
Give another definition, whithout using occ, and compare
the ease of
development in the two approaches. You should be able to redo the all
development with the new definitions.
This file contains some lemmas
which establish the relationship between both definitions. You should be
able to build a development similar to using