Verify Evaluate Opt eqv verify Evaluate ok

theorem verifyEvaluateOpt_eqv_verifyEvaluate_ok {p wp : Policy} {cp : CompiledPolicy} {Γ : Validation.TypeEnv} {φ : Term → Term} :  CompiledPolicy.compile p Γ = .ok cp →  wellTypedPolicy p Γ = .ok wp →  verifyEvaluate φ wp (SymEnv.ofTypeEnv Γ) ~ .ok (verifyEvaluateOpt φ cp):= by  simp [verifyEvaluate, verifyEvaluateOpt, ResultAssertsEquiv]  intro h₀ h₁  simp [enforceCompiledPolicy_eqv_enforce_ok h₀ h₁]  cases h₂ : compile wp.toExpr (SymEnv.ofTypeEnv Γ) <;> simp  case error e =>    simp only [CompiledPolicy.compile, Except.mapError, h₁, Except.bind_ok] at h₀    rw [Opt.compile.correctness] at h₀    simp [h₂] at h₀  case ok t =>    have h₃ := (cp_compile_produces_the_right_term h₀ h₁).symm ; simp [h₂] at h₃ ; subst t    split <;> rename_i hnot    · apply Asserts.Equiv.constantFalse <;> simp [hnot]    · apply Asserts.Equiv.rfl