rw [← hf.indep.mem_cl_iff_of_not_mem hef, he.parallel_iff_mem_cl]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
hf : M.Nonloop f
hef : e ≠ f
⊢ M.Parallel e f ↔ M.Dep {e, f}
no goals