rwa [contract_contract, inter_union_diff] at hwin
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
no goals