refine eq_of_indep_iff_indep_forall (by simp [diff_diff_comm]) (fun I hI ↦ ?_)
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
⊢ M ／ C ＼ D = M ＼ D ／ C
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : I ⊆ (M ／ C ＼ D).E
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I