Add lift_functional_correctness

This lemma makes proving simple properties about the deployed contract
state of a contract easier.
4 jobs for master in 4 minutes and 25 seconds (queued for 1 second)