Verify Never Matches is sound

theorem verifyNeverMatches_is_sound' {p : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p →  verifyNeverMatches 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 := verifyNeverMatches_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,    List.filterMap_nil, Bool.not_eq_eq_eq_not, Bool.not_true, beq_eq_false_iff_ne, ne_eq]  cases p.effect <;> simp [Data.Set.make_nil, Data.Set.not_mem_empty, this]