Verify Never Errors is ok and complete

theorem verifyNeverErrors_is_ok_and_complete {p p' : Policy} {Γ : TypeEnv} :  Γ.WellFormed →  wellTypedPolicy p Γ = .ok p' →  ∃ asserts,    verifyNeverErrors 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).isOk):= by  intros hwf hwt  have hwf_εnv := ofEnv_swf_for_policy hwf hwt  have ⟨asserts, hok⟩ := verifyNeverErrors_is_ok hwf hwt  exists asserts  simp only [hok, true_and]  intros hsat  have ⟨env, hmodel, hswf_env, henum_comp, hres⟩ := verifyNeverErrors_is_complete 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