Changing inductive definitions
In chap11.v , the predicates
min and maj are 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.
Solution
This file contains some lemmas
which establish the relationship between both definitions. You should be
able to build a development similar to using
these lemmas.