Verify Always Matches is sound

theorem verifyAlwaysMatches_is_sound' {p : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p →  verifyAlwaysMatches p εnv = .ok asserts →  εnv ⊭ asserts →  ∀ env,    env ∈ᵢ εnv →    env.StronglyWellFormedForPolicy p →    p.id ∈ (Spec.isAuthorized env.request env.entities [p]).determiningPolicies:= by  intro h₁ h₂ h₃ env h₄ h₅  have := verifyAlwaysMatches_is_sound h₁ h₂ h₃ env h₄ h₅  simp only [Spec.isAuthorized, Data.Set.isEmpty, Spec.satisfiedPolicies, satisfiedWithEffect,    satisfied, Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq, List.filterMap_cons, this, and_true,    List.filterMap_nil, Bool.not_eq_eq_eq_not, Bool.not_true, beq_eq_false_iff_ne, ne_eq]  cases p.effect <;> simp