simp [restrict_parallel_iff, hef, he, hf]
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : (M ↾ X).Simple
he : e ∈ X
hf : f ∈ X
hef : M.Parallel e f
⊢ (M ↾ X).Parallel ↑⟨e, he⟩ ↑⟨f, hf⟩
no goals