changed the behavior of Cnf.miniscope (with a flag to enable old behavior): try
to keep scope of existential quantification large