Fix lift Var case
Give first lift lemma a proper name, remove fishiness