Validation is sound response

theorem validation_is_sound_response (policies : Policies) (schema : Schema) (request : Request) (entities : Entities)  (huniq : PolicyIdsUnique policies)  (hwf : schema.validateWellFormed = .ok ())  (hv : validate policies schema = .ok ())  (hr : validateRequest schema request = .ok ())  (he : validateEntities schema entities = .ok ()) :  ∀ p ∈ policies, p.id ∈ (isAuthorized request entities policies).erroringPolicies →    evaluate p.toExpr request entities = .error .entityDoesNotExist ∨    evaluate p.toExpr request entities = .error .extensionError ∨    evaluate p.toExpr request entities = .error .arithBoundsError:= by  intro p hp hmem  obtain ⟨p', hp', hid, e, herr⟩ := error_of_mem_erroringPolicies hmem  have hpeq : p' = p := huniq p' hp' p hp hid  rw [hpeq] at herr  have hsound : AllEvaluateToBool policies request entities :=    validation_is_sound policies schema request entities hwf hv hr he  have hev : EvaluatesToBool p.toExpr request entities := hsound p hp  obtain ⟨b, hev⟩ := hev  unfold EvaluatesTo at hev  rcases hev with h | h | h | h  · exact Or.inl h  · exact Or.inr (Or.inl h)  · exact Or.inr (Or.inr h)  · rw [herr] at h; exact absurd h (by simp)