We changed the prepare_for_counterexamples transformation to allow
printing of quantified expressions, remove duplications of printed
examples and adding an incomplete function to print universally
quantified variables that are positive but not at head of the term.

* src/transform/intro_projections_counterexmp.ml
(intro_const_equal_to_term): Generating of the preid for a counterex.

* src/transform/intro_projections_counterexmp.mli
(val_intro_const_equal_to_term): Changing signature.

* src/transform/intro_vc_vars_counterexmp.ml
(Hprid): Adding a container for preids.
(do_intro): Adding cases for generation of counterexample in the Tvar
case, factorising the construction of vc_constant in a function
new_counter_example_variable. Adding argument vc_map to avoid
duplication of vc_constants
(new_counter_example_variable): Adding a check to avoid duplication of
vc_constant.
(remove_positive_foralls): New experimental incomplete function that aims
at introducting foralls even when they are under a construct.
"H /\ forall i. P(i)" becomes "i as premisse and H /\ P(i)".
(intros): Added calls to do_intro and removed optimizations.
(do_intro_vc_vars_counterexmp): Concatenate results of intros and
do_intros and create the prop goal.

* src/transform/introduction.ml
(stop_intro): Removed stop_intro.

* src/transform/prepare_for_counterexmp.ml
(prepare_for_counterexmp2): Removed call to introduce_premisses.

Change-Id: I836ae9e69b887247eb64196705cc7ad32ba36825