HomeIsabelle/Phabricator

factored out lemmas