HomeIsabelle/Phabricator

tuned proofs -- avoid z3;