Add one admitted lift_lift_rev lemma

Proof shamefully copy-pasted from dblib.