o z3_code now does part of the generic instantiation of hypotheses
o added a test case, computation calculus in which the everywhere operator is needed. The support for the operator is not complete yet.