HomeIsabelle/Phabricator

fixed lemma following Isabelle/c256bba593f3