HomeIsabelle/Phabricator

added lemma multpHO_implies_one_step_strong