Evaluate Policy ok implies well formed env

theorem evaluatePolicy_ok_implies_well_formed_env  {schema : Schema} {p : Policy} {req : Request} {es : Entities} {r : Residual} :  evaluatePolicy schema p req.asPartialRequest Map.empty = .ok r →  schema.validateWellFormed = .ok () →  validateEntities schema es = .ok () →  ∃ env,    schema.environment? req.asPartialRequest.principal.ty req.asPartialRequest.resource.ty req.asPartialRequest.action = .some env ∧    InstanceOfWellFormedEnvironment req es env:= by  intro h_ep h_schema_wf h_entities  obtain ⟨env, h_env⟩ := evaluatePolicy_ok_implies_env_some h_ep  have h_mem := environment_some_mem_environments h_env  exact ⟨env, h_env, instance_of_well_formed_env    (List.forM_ok_implies_all_ok _ _ h_schema_wf _ h_mem)    (evaluatePolicy_ok_implies_requestMatchesEnvironment h_ep env h_env)    (List.forM_ok_implies_all_ok _ _ h_entities _ h_mem)⟩