HomeIsabelle/Phabricator

removal of a redundant theorem (and white space)