HomeIsabelle/Phabricator

added a lemma about grounding in ordered resolution prover