Factoring out & generifying LemmaApply

- previously implemented in Auto/AutoProver2