{α : Type u_1} →
  [inst : CompleteLattice α] →
    {S : Set α} →
      {motive : IsCompactlyGenerated.BooleanGenerators S → Sort u} →
        (t : IsCompactlyGenerated.BooleanGenerators S) →
          ((isAtom : ∀ I ∈ S, IsAtom I) →
              (finitelyAtomistic :
                  ∀ (s : Finset α) (a : α), ↑s ⊆ S → IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id) →
                motive ⋯) →
            motive t