Unchanged erroring when add policy

theorem unchanged_erroring_when_add_policy (request: Request) (entities: Entities) (policies : Policies) (policy₀ : Policy) :  (isAuthorized request entities policies).erroringPolicies ⊆ (isAuthorized request entities (policy₀ :: policies)).erroringPolicies  := by  unfold isAuthorized  simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true]  split <;> split  all_goals {    unfold errorPolicies    simp only [List.filterMap_cons]    cases errored policy₀ request entities    · simp only [Set.subset_def, imp_self, implies_true]    · rw [Set.make_cons_eq_singleton_union, Set.union_comm]; apply Set.subset_union  }