Verify Never Matches is ok and complete

theorem verifyNeverMatches_is_ok_and_complete {p p' : Policy} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicy p Γ = .ok p' →  ∃ asserts,    verifyNeverMatches p' (SymEnv.ofEnv Γ) = .ok asserts ∧    (SymEnv.ofEnv Γ ⊧ asserts →      ∃ env : Env,        InstanceOfWellFormedEnvironment env.request env.entities Γ ∧        env.StronglyWellFormedForPolicy p' ∧        evaluate p.toExpr env.request env.entities = .ok (.prim (.bool true))):= by  intros hwf hwt  have hwf_εnv := ofEnv_swf_for_policy hwf hwt  have ⟨asserts, hok⟩ := verifyNeverMatches_is_ok hwf hwt  exists asserts  simp only [hok, true_and]  intros hsat  have ⟨env, hmodel, hswf_env, henum_comp, hres⟩ := verifyEvaluate_is_complete verifyNeverMatches_wbeq hwf_εnv hok hsat  have hinst := ofEnv_completeness hwf hswf_env.1 henum_comp hmodel  have := wellTypedPolicy_preserves_evaluation hinst hwt  simp only [←wellTypedPolicy_preserves_evaluation hinst hwt] at hres  exists env  simp [this] at hres  simp [*]