∀ {α : Type u_1} {M : Matroid α} {B : Set α}
  (motive :
    ((∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
        ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y) →
      Prop)
  (x :
    (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y),
  (∀ (B' : Set α) (hB' : M.IsBase B') (hBB' : Disjoint B B')
      (h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y), motive ⋯) →
    motive x