∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (parts parts_1 : Finset α) (e_parts : parts = parts_1)
  (supIndep : parts.SupIndep id) (sup_parts : parts.sup id = a) (bot_notMem : ⊥ ∉ parts),
  { parts := parts, supIndep := supIndep, sup_parts := sup_parts, bot_notMem := bot_notMem } =
    { parts := parts_1, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }