Continuing fixing nested but convertible occurrences in find_subterm
(see 2e3ae20fe1e): test was only relevant in the case of explicitly
given occurrence numbers.
Option -type-in-type continued (deactivate test for inferred sort of
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
Slightly improving error messages when mismatch with Proof using at Qed time.
Making map_union a standard function of the ML library.