HomeIsabelle/Phabricator

refactoring to make parts of proof reusable to ongoing formalization