Verify Never Errors is ok and sound

theorem verifyNeverErrors_is_ok_and_sound {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 hunsat env hinst hwf_env  simp only [wellTypedPolicy_preserves_evaluation hinst hwt]  apply verifyNeverErrors_is_sound hwf_εnv hok hunsat env  · exact ofEnv_soundness hwf_env.1 hinst  · exact hwf_env