simpa using h I
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
x✝¹ : M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
hE : M.E = E
h : ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
I : Set α
x✝ : I ⊆ M.E
⊢ M.Indep I ↔ (unifOn E k).Indep I
no goals