rw [pair_diff_right hef]
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep ({e, x} \ {x})
case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep {e}