exact ⟨toNonloop ⟨hef.mem_ground_left, heC⟩, toNonloop ⟨hef.mem_ground_right, hfC⟩⟩
case neg.a
α : 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
⊢ (M ／ C).Nonloop e ∧ (M ／ C).Nonloop f
no goals