{α : Type u_2} →
  {motive : IndepMatroid α → Sort u} →
    (t : IndepMatroid α) →
      ((E : Set α) →
          (Indep : Set α → Prop) →
            (indep_empty : Indep ∅) →
              (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
                (indep_aug :
                    ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) →
                  (indep_maximal : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X) →
                    (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) →
                      motive
                        { E := E, Indep := Indep, indep_empty := indep_empty, indep_subset := indep_subset,
                          indep_aug := indep_aug, indep_maximal := indep_maximal, subset_ground := subset_ground }) →
        motive t