simp_rw [eq_unifOn_iff, delete_ground, unifOn_ground_eq, true_and, delete_indep_iff,
  unifOn_indep_iff, subset_diff, and_assoc, imp_true_iff]
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E D : Set α
k : ℕ∞
⊢ unifOn E k ＼ D = unifOn (E \ D) k
no goals