import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Powerset
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Tactic.NormNum

def OA_statement : Prop := (∀ (xs ys : List (Finset Nat)), xs.toFinset = ys.toFinset →
 xs.foldr (fun update state => update ∪ state) ∅ =
 ys.foldr (fun update state => update ∪ state) ∅)

theorem OA_target : OA_statement :=
  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]

#print axioms OA_target
#check OA_target