HomeIsabelle/Phabricator

two new theorems