HomeIsabelle/Phabricator

tuned lemma by dropping one assumption