Verify Evaluate Pair Opt eqv verify Evaluate Pair ok

theorem verifyEvaluatePairOpt_eqv_verifyEvaluatePair_ok {p₁ p₂ wp₁ wp₂ : Policy} {cp₁ cp₂ : CompiledPolicy} {Γ : Validation.TypeEnv} {φ : Term → Term → Term} :  CompiledPolicy.compile p₁ Γ = .ok cp₁ →  CompiledPolicy.compile p₂ Γ = .ok cp₂ →  wellTypedPolicy p₁ Γ = .ok wp₁ →  wellTypedPolicy p₂ Γ = .ok wp₂ →  verifyEvaluatePair φ wp₁ wp₂ (SymEnv.ofTypeEnv Γ) ~ .ok (verifyEvaluatePairOpt φ cp₁ cp₂):= by  simp [verifyEvaluatePair, verifyEvaluatePairOpt, ResultAssertsEquiv]  intro h₀ h₁ h₂ h₃  have henv : cp₁.εnv = cp₂.εnv := by    simp [cp_compile_produces_the_right_env h₀, cp_compile_produces_the_right_env h₁]  simp [henv]  simp [enforcePairCompiledPolicy_eqv_enforce_ok h₀ h₁ 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₁    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