Skip to content

Update Proofs/Script_....v

Update the remaining proofs files for Michelson Script_....v, removing the equality lemmas on the simulations, and moving the validity lemmas to OCaml functions instead of the simulations. Admit all the proofs unless if very simple.