HomeIsabelle/Phabricator

Shortened several messy proofs