HomeIsabelle/Phabricator

formal position for spec rule (not significant for equality);