move things back to cakeml, and finish proof of proveHyp