Verify Matches Implies is ok and complete

theorem verifyMatchesImplies_is_ok_and_complete {p₁ p₁' p₂ p₂' : Policy} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicy p₁ Γ = .ok p₁' →  wellTypedPolicy p₂ Γ = .ok p₂' →  ∃ asserts,    verifyMatchesImplies 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⟩ := verifyMatchesImplies_is_ok hwf hwt₁ hwt₂  exists asserts  simp only [hok, true_and]  intros hsat  have ⟨env, hmodel, hswf_env₁, hswf_env₂, henum_comp, hres⟩ := verifyMatchesImplies_is_complete hwf_εnv₁ hwf_εnv₂ hok hsat  have hinst := ofEnv_completeness hwf hswf_env₁.1 henum_comp hmodel  simp only [    ←wellTypedPolicy_preserves_evaluation hinst hwt₁,    ←wellTypedPolicy_preserves_evaluation hinst hwt₂,  ] at hres  exists env