obtain ⟨hCl, hC⟩ := hC
case intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D C : Set α
hC : (M ↾ C).Loopless ∧ ∀ (e f : α), (M ↾ C).Parallel e f → e = f
hl : (M ／ C).Loopless
h : ∀ (e f : α), (M ／ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
case intro.intro
α : 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 ↾ C).Parallel e f → e = f
⊢ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f