HomeIsabelle/Phabricator

retain derived lemma for better findability