Verify Evaluate Pair is ok

theorem verifyEvaluatePair_is_ok {φ : Term → Term → Term} {p₁ p₁' p₂ p₂' : Policy} {Γ : TypeEnv}  (hwf : Γ.WellFormed)  (hwt₁ : wellTypedPolicy p₁ Γ = .ok p₁')  (hwt₂ : wellTypedPolicy p₂ Γ = .ok p₂') :  ∃ asserts, verifyEvaluatePair φ p₁' p₂' (SymEnv.ofEnv Γ) = .ok asserts:= by  have ⟨tx₁, hwt_tx₁, heq_tx₁⟩ := wellTypedPolicy_ok_implies_well_typed_expr hwt₁  have ⟨tx₂, hwt_tx₂, heq_tx₂⟩ := wellTypedPolicy_ok_implies_well_typed_expr hwt₂  simp only [verifyEvaluatePair]  have ⟨_, hok₁, _⟩ := compile_well_typed hwf hwt_tx₁  have ⟨_, hok₂, _⟩ := compile_well_typed hwf hwt_tx₂  simp only [heq_tx₁, heq_tx₂] at hok₁ hok₂  simp [hok₁, hok₂]