Verify Always Allows is ok and sound

theorem verifyAlwaysAllows_is_ok_and_sound {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 hunsat env hinst hwf_ps₁  simp only [    wellTypedPolicies_preserves_isAuthorized hinst hwt₁,  ]  apply verifyAlwaysAllows_is_sound hwf_εnv₁ hok hunsat env _ hwf_ps₁  exact ofEnv_soundness hwf_ps₁.1 hinst