Added lifting lemmas for the quantifier pulling. Everything should be in
place now.