Verify Matches Equivalent is complete

theorem verifyMatchesEquivalent_is_complete {p₁ p₂ : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p₁ →  εnv.StronglyWellFormedForPolicy p₂ →  verifyMatchesEquivalent p₁ p₂ εnv = .ok asserts →  εnv ⊧ asserts →  ∃ env,    env ∈ᵢ εnv ∧    env.StronglyWellFormedForPolicy p₁ ∧    env.StronglyWellFormedForPolicy p₂ ∧    Env.EnumCompleteFor env εnv ∧    (evaluate p₁.toExpr env.request env.entities = .ok true) ≠    (evaluate p₂.toExpr env.request env.entities = .ok true):= by  intro h₁ h₂ h₃ h₄  have ⟨env, h₅, h₆, h₇, h₈, h₉⟩ := verifyEvaluatePair_is_complete verifyMatchesEquivalent_wbepq h₁ h₂ h₃ h₄  exists env  simp only [beq_eq_false_iff_ne, ne_eq] at h₉  apply And.intro h₅  apply And.intro h₆  apply And.intro h₇  apply And.intro h₈  cases hev₁ : evaluate p₁.toExpr env.request env.entities == .ok (.prim (.bool true))  · simp only [hev₁, Bool.false_eq, beq_eq_false_iff_ne, ne_eq, Decidable.not_not] at h₉    simp only [beq_eq_false_iff_ne, ne_eq] at hev₁    simp [*]  · simp only [hev₁, Bool.true_eq, beq_iff_eq] at h₉    simp only [beq_iff_eq] at hev₁    simp [*]