theorem Set.mem_sUnion._simp_1
theorem Set.mem_sUnion._simp_1
: ∀ {α : Type u} {x : α} {S : zpg9xh52.Set (zpg9xh52.Set α)},
  Membership.mem (zpg9xh52.Set.sUnion S) x = ∃ t, Membership.mem S t ∧ Membership.mem t x