refine eq_of_base_iff_base_forall rfl (fun B _ ↦ ?_)
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (unif a (a + b))✶ = unif b (a + b)
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ (unif a (a + b))✶.Base B ↔ (unif b (a + b)).Base B