Verify Is Authorized Opt eqv verify Is Authorized ok

theorem verifyIsAuthorizedOpt_eqv_verifyIsAuthorized_ok {ps₁ ps₂ wps₁ wps₂ : Policies} {cpset₁ cpset₂ : CompiledPolicySet} {Γ : Validation.TypeEnv} {φ : Term → Term → Term} :  CompiledPolicySet.compile ps₁ Γ = .ok cpset₁ →  CompiledPolicySet.compile ps₂ Γ = .ok cpset₂ →  wellTypedPolicies ps₁ Γ = .ok wps₁ →  wellTypedPolicies ps₂ Γ = .ok wps₂ →  verifyIsAuthorized φ wps₁ wps₂ (SymEnv.ofTypeEnv Γ) ~ .ok (verifyIsAuthorizedOpt φ cpset₁ cpset₂):= by  simp [verifyIsAuthorized, verifyIsAuthorizedOpt, ResultAssertsEquiv]  intro hcpset₁ hcpset₂ hwps₁ hwps₂  simp [enforcePairCompiledPolicySet_eqv_enforce_ok hcpset₁ hcpset₂ hwps₁ hwps₂]  have henvs : cpset₁.εnv = cpset₂.εnv := by    simp [cpset_compile_produces_the_right_env hcpset₁, cpset_compile_produces_the_right_env hcpset₂]  simp [henvs]  cases h₁ : SymCC.isAuthorized wps₁ (SymEnv.ofTypeEnv Γ) <;> simp  case error e =>    simp_all only [CompiledPolicySet.compile, Except.mapError, Except.bind_ok]    rw [Opt.isAuthorized.correctness] at hcpset₁    simp [h₁] at hcpset₁  case ok t =>    have h₃ := (cpset_compile_produces_the_right_term hcpset₁ hwps₁).symm ; simp [h₁] at h₃ ; subst t    cases h₂ : SymCC.isAuthorized wps₂ (SymEnv.ofTypeEnv Γ) <;> simp    case error e =>      simp_all only [CompiledPolicySet.compile, Except.mapError, Except.bind_ok]      rw [Opt.isAuthorized.correctness] at hcpset₂      simp [h₂] at hcpset₂    case ok t =>      have h₃ := (cpset_compile_produces_the_right_term hcpset₂ hwps₂).symm ; simp [h₂] at h₃ ; subst t      split <;> rename_i hnot      · apply Asserts.Equiv.constantFalse <;> simp [hnot]      · apply Asserts.Equiv.rfl