HomeIsabelle/Phabricator

more explicit proof