Verify Matches Disjoint is sound

theorem verifyMatchesDisjoint_is_sound {p₁ p₂ : Policy} {εnv : SymEnv} {asserts : Asserts} :  εnv.StronglyWellFormedForPolicy p₁ →  εnv.StronglyWellFormedForPolicy p₂ →  verifyMatchesDisjoint 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 := verifyEvaluatePair_is_sound verifyMatchesDisjoint_wbepq h₁ h₂ h₃ h₄ env h₅ h₆ h₇  simp only [Bool.not_and, Bool.or_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true,    beq_eq_false_iff_ne, ne_eq] at this  cases this with  | inl h => simp [h]  | inr h => simp [h]