HomeIsabelle/Phabricator

added a couple of structured proofs