HomeIsabelle/Phabricator

Removal of some needless finiteness assumptions