rw [← diff_union_of_subset hCC', union_comm, ← contract_contract]
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C' ≤m M ／ 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 C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C ／ (C' \ C) ≤m M ／ C