by
  have collapse : ∀ (xs : List (Finset Nat)), xs.foldr (fun update state => update ∪ state) ∅ = xs.toFinset.sup id := by
    intro xs
    induction xs with
    | nil => simp
    | cons x xs ih => simp [ih, Finset.sup_insert]
  intro xs ys equal
  rw [collapse, collapse, equal]