{α : Type u_1} →
  {M : Matroid α} →
    {motive : M.Finitary → Sort u} →
      ((indep_of_forall_finite : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I) → motive ⋯) →
        (t : M.Finitary) → motive t