Validation is sound

theorem validation_is_sound (policies : Policies) (schema : Schema) (request : Request) (entities : Entities) :  schema.validateWellFormed = .ok () →  validate policies schema = .ok () →  validateRequest schema request = .ok () →  validateEntities schema entities = .ok () →  AllEvaluateToBool policies request entities:= by  intro hwf h₀ h₁ h₂  have h₁ := request_and_entities_validate_implies_instance_of_wf_schema schema request entities hwf h₁ h₂  unfold validate at h₀  simp only [AllEvaluateToBool]  cases h₃ : policies with  | nil => simp only [List.not_mem_nil, false_implies, implies_true]  | cons h' t' =>    intro policy pin    simp only [EvaluatesToBool]    apply typecheck_policy_with_environments_is_sound policy schema request entities h₁    subst h₃    simp only [List.forM_eq_forM, List.forM_cons] at h₀    simp_do_let (typecheckPolicyWithEnvironments typecheckPolicy h' schema) as h₄ at h₀    case ok _ =>      rw [List.mem_cons] at pin      cases pin with      | inl h₅ =>        subst h₅        exact h₄      | inr h₅ =>        apply List.forM_ok_implies_all_ok t' (typecheckPolicyWithEnvironments _ · schema)        repeat assumption