HomeIsabelle/Phabricator

Two new lemmas by Eberl (requested by Paulson)