Add one more admitted lift_lift_rev lemma

Proof shamefully copy-pasted from dblib.