Transformation intro_projections_counterexmp introduce new constant c
and axiom for all abstract functions and predicates p labeled with
label "model_projected", not only for these for that there exists
projection function. If the projection function does not exist,
the axiom states c = p, if there exists projection function f,
the axiom states c = f p.