Certified search trees
Consider the development in chap11.v .
Define a type for certified search trees , then
consider new specifications for occur test, insertion and deletion.
Solution
The development search_set.v
contains the definition of a type sch_tree in sort
Set, and defines new specifications named
sch_insert_spec, sch_rm_spec, etc.
It ends with two functions transforming the older specifications into the
new ones, and viceversa.