{α : Type u_1} →
  [inst : Preorder α] →
    {motive : LocallyFiniteOrder α → Sort u} →
      (t : LocallyFiniteOrder α) →
        ((finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α) →
            (finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) →
              (finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ a ≤ x ∧ x < b) →
                (finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ a < x ∧ x ≤ b) →
                  (finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ a < x ∧ x < b) →
                    motive
                      { finsetIcc := finsetIcc, finsetIco := finsetIco, finsetIoc := finsetIoc, finsetIoo := finsetIoo,
                        finset_mem_Icc := finset_mem_Icc, finset_mem_Ico := finset_mem_Ico,
                        finset_mem_Ioc := finset_mem_Ioc, finset_mem_Ioo := finset_mem_Ioo }) →
          motive t