boehmes [Wed, 09 Mar 2011 21:40:38 +0100] rev 41899
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)