HomeIsabelle/Phabricator

trying to streamline a few proofs