HomeIsabelle/Phabricator

slightly less abusive proof pattern