Verify Matches Equivalent is sound

theorem verifyMatchesEquivalent_is_sound {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₂ →    (evaluate p₁.toExpr env.request env.entities = .ok true) =    (evaluate p₂.toExpr env.request env.entities = .ok true):= by  intro h₁ h₂ h₃ h₄ env h₅ h₆ h₇  have h_sound := verifyEvaluatePair_is_sound verifyMatchesEquivalent_wbepq h₁ h₂ h₃ h₄ env h₅ h₆ h₇  rw [beq_iff_eq] at h_sound  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] at h_sound    simp only [beq_eq_false_iff_ne, ne_eq] at hev₁    simp [*]  · simp only [hev₁, Bool.true_eq, beq_iff_eq] at h_sound    simp only [beq_iff_eq] at hev₁    simp [*]