Verify Always Allows Opt eqv verify Always Allows ok

theorem verifyAlwaysAllowsOpt_eqv_verifyAlwaysAllows_ok {ps wps : Policies} {cpset : CompiledPolicySet} {Γ : Validation.TypeEnv} :  CompiledPolicySet.compile ps Γ = .ok cpset →  wellTypedPolicies ps Γ = .ok wps →  verifyAlwaysAllows wps (SymEnv.ofTypeEnv Γ) ~ .ok (verifyAlwaysAllowsOpt cpset):= by  simp [verifyAlwaysAllows, verifyAlwaysAllowsOpt]  intro hcpset hwps  apply verifyImpliesOpt_eqv_verifyImplies_ok _ hcpset (wellTypedPolicies_allowAll Γ) hwps  simp [CompiledPolicySet.compile, Except.mapError, do_eq_ok, wellTypedPolicies_allowAll]  rw [Opt.isAuthorized.correctness]  simp [isAuthorized_allowAll, footprint_allowAll, CompiledPolicySet.allowAll, cpset_compile_produces_the_right_env hcpset, footprints_singleton, Data.Set.map_empty]