HomeIsabelle/Phabricator

tuned proofs -- more stable proof terms without [rule_format];