Verify Matches Implies is sound

theorem verifyMatchesImplies_is_sound {p₁ p₂ : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p₁ →  εnv.StronglyWellFormedForPolicy p₂ →  verifyMatchesImplies 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₇ h₈  have := verifyEvaluatePair_is_sound verifyMatchesImplies_wbepq h₁ h₂ h₃ h₄ env h₅ h₆ h₇  simp only [Bool.or_eq_true, bne_iff_ne, ne_eq, beq_iff_eq] at this  cases this with  | inl h => contradiction  | inr h => exact h