HomeIsabelle/Phabricator

weakened assumption a tiny bit (syntactically; semantically this is the same)