Verify Always Matches is complete

theorem verifyAlwaysMatches_is_complete {p : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p →  verifyAlwaysMatches p εnv = .ok asserts →  εnv ⊧ asserts →  ∃ env,    env ∈ᵢ εnv ∧    env.StronglyWellFormedForPolicy p ∧    Env.EnumCompleteFor env εnv ∧    evaluate p.toExpr env.request env.entities ≠ .ok true:= by  intro h₁ h₂ h₃  unfold verifyAlwaysMatches at h₂  have ⟨env, h₄, h₅, h₆, h₇⟩ := verifyEvaluate_is_complete verifyAlwaysMatches_wbeq h₁ h₂ h₃  exists env  rw [beq_eq_false_iff_ne, ne_eq] at h₇  exact ⟨h₄, h₅, h₆, h₇⟩