improving term postprocessing for counterexample presentation in quickcheck

tuned

finished and tested Z3 proof reconstruction for injective functions;
only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)

improved formula for specialization, to prevent needless specializations -- and removed dead code

perform no arity check in debug mode so that we get to see the Kodkod problem

spark_end now joins proofs of VCs before writing *.prv file.

clarified

produce helpful mira summary for more errors

eliminated prems;

eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;