Verify Matches Equivalent is ok and sound

theorem verifyMatchesEquivalent_is_ok_and_sound {p₁ p₁' p₂ p₂' : Policy} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicy p₁ Γ = .ok p₁' →  wellTypedPolicy p₂ Γ = .ok p₂' →  ∃ asserts,    verifyMatchesEquivalent p₁' p₂' (SymEnv.ofEnv Γ) = .ok asserts ∧    (SymEnv.ofEnv Γ ⊭ asserts →      ∀ env : Env,        InstanceOfWellFormedEnvironment env.request env.entities Γ →        env.StronglyWellFormedForPolicy p₁' →        env.StronglyWellFormedForPolicy p₂' →        (evaluate p₁.toExpr env.request env.entities = .ok (.prim (.bool true))) =        (evaluate p₂.toExpr env.request env.entities = .ok (.prim (.bool true)))):= by  intros hwf hwt₁ hwt₂  have hwf_εnv₁ := ofEnv_swf_for_policy hwf hwt₁  have hwf_εnv₂ := ofEnv_swf_for_policy hwf hwt₂  have ⟨asserts, hok⟩ := verifyMatchesEquivalent_is_ok hwf hwt₁ hwt₂  exists asserts  simp only [hok, true_and]  intros hunsat env hinst hwf_env₁ hwf_env₂  simp only [    wellTypedPolicy_preserves_evaluation hinst hwt₁,    wellTypedPolicy_preserves_evaluation hinst hwt₂,  ]  apply verifyMatchesEquivalent_is_sound hwf_εnv₁ hwf_εnv₂ hok hunsat env _ hwf_env₁ hwf_env₂  exact ofEnv_soundness hwf_env₁.1 hinst