simpa
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
this : ∀ I ⊆ E, I = ∅ → I.encard ≤ k
⊢ ∀ I ⊆ ((loopyOn E).truncateTo k).E, ((loopyOn E).truncateTo k).Indep I ↔ (loopyOn E).Indep I
no goals