refine eq_of_indep_iff_indep_forall rfl ?_
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.truncateTo 0 = loopyOn M.E
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I