exact hC _ _ hef heC hfC
case pos
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D C : Set α
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
hCl : (M ↾ C).Loopless
hC : ∀ (e f : α), M.Parallel e f → e ∈ C → f ∈ C → e = f
e f : α
hef : M.Parallel e f
heC : e ∈ C
hfC : f ∈ C
⊢ e = f
no goals