Add one more lift_lift_rev lemma

Proof shamefully copy-pasted from dblib.