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)
Status Job ID Name Coverage
  Build
passed #101593
au
coq:8.10

00:03:50

failed #101591
au
coq:8.8

00:00:34

failed #101592
au
coq:8.9

00:00:38

passed #101594
au
coq:dev

00:03:40

 
Name Stage Failure
failed
coq:8.9 Build
ocamlfind      1.8.1          A library manager for OCaml
opam-depext 1.1.3 Query and install external dependencies of OPAM packages
$ opam install coq-stdpp
The following actions will be performed:
- install coq-stdpp dev.2019-10-07.0.e35c9837
- install conf-findutils 1
===== 2 to install =====
Do you want to continue? [Y/n] n
ERROR: Job failed: exit code 1
failed
coq:8.8 Build
ocamlfind      1.8.1          A library manager for OCaml
opam-depext 1.1.3 Query and install external dependencies of OPAM packages
$ opam install coq-stdpp
The following actions will be performed:
- install coq-stdpp dev.2019-10-07.0.e35c9837
- install conf-findutils 1
===== 2 to install =====
Do you want to continue? [Y/n] n
ERROR: Job failed: exit code 1