HomeIsabelle/Phabricator

A slightly stronger lemma allowing slightly simpler proofs