Verify Matches Disjoint is complete

theorem verifyMatchesDisjoint_is_complete {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₂ ∧    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 verifyMatchesDisjoint_wbepq h₁ h₂ h₃ h₄  exists env  simp only [Bool.not_and, Bool.or_eq_false_iff, Bool.not_eq_eq_eq_not, Bool.not_false,    beq_iff_eq] at h₉  simp [*]