HomeIsabelle/Phabricator

Moved a number of general-purpose lemmas into HOL