Verify Always Allows is ok and complete

theorem verifyAlwaysAllows_is_ok_and_complete {ps₁ ps₁' : Policies} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicies ps₁ Γ = .ok ps₁' →  ∃ asserts,    verifyAlwaysAllows ps₁' (SymEnv.ofEnv Γ) = .ok asserts ∧    (SymEnv.ofEnv Γ ⊧ asserts →      ∃ env : Env,        InstanceOfWellFormedEnvironment env.request env.entities Γ ∧        env.StronglyWellFormedForPolicies ps₁' ∧        ¬ allows (Spec.isAuthorized env.request env.entities ps₁)):= by  intros hwf hwt₁  have hwf_εnv₁ := ofEnv_swf_for_policies hwf hwt₁  have ⟨asserts, hok⟩ := verifyAlwaysAllows_is_ok hwf hwt₁  exists asserts  simp only [hok, true_and]  intros hsat  have ⟨env, hmodel, hswf_env₁, henum_comp, hres⟩ := verifyAlwaysAllows_is_complete hwf_εnv₁ hok hsat  have hinst := ofEnv_completeness hwf hswf_env₁.1 henum_comp hmodel  simp only [    ←wellTypedPolicies_preserves_isAuthorized hinst hwt₁,  ] at hres  exists env