HomeIsabelle/Phabricator

simplified proof