Unchanged determining when add policy and decision unchanged

theorem unchanged_determining_when_add_policy_and_decision_unchanged (request: Request) (entities: Entities) (policies: Policies) (policy₀ : Policy) :  let auth  := (isAuthorized request entities policies)  let auth' := (isAuthorized request entities (policy₀ :: policies))  auth.decision = auth'.decision → auth.determiningPolicies ⊆ auth'.determiningPolicies  := by  intro auth auth' h₀  have subset_lemma : ∀ effect, satisfiedPolicies effect policies request entities ⊆                                 satisfiedPolicies effect (policy₀ :: policies) request entities := by    intro effect    unfold satisfiedPolicies    rw [List.filterMap_cons]    cases satisfiedWithEffect effect 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  rw [determiningPolicies_of request entities policies,      determiningPolicies_of request entities (policy₀ :: policies)]  simp only [h₀, auth]  apply subset_lemma