Add one more lift_lift_rev lemma

Proof shamefully copy-pasted from dblib.
Merge pull request #19 from knuton/more_lift

Add one admitted lift_lift_rev lemma