Verify Never Matches is complete

theorem verifyNeverMatches_is_complete' {p : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p →  verifyNeverMatches p εnv = .ok asserts →  εnv ⊧ asserts →  ∃ env,    env ∈ᵢ εnv ∧    env.StronglyWellFormedForPolicy p ∧    Env.EnumCompleteFor env εnv ∧    p.id ∈ (Spec.isAuthorized env.request env.entities [p]).determiningPolicies:= by  intro h₁ h₂ h₃  have ⟨env, h₄, h₅, h₆, h₇⟩ := verifyNeverMatches_is_complete h₁ h₂ h₃  exists env  apply And.intro h₄  apply And.intro h₅  apply And.intro 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, h₇, 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