rintro rfl
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ f✝ : α
heE : e✝ ∈ M.E
⊢ e✝ = f✝ → M.Parallel e✝ f✝
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f
left✝ : M.Loopless
h : ∀ (e f : α), M.Parallel e f → e = f
e✝ : α
heE : e✝ ∈ M.E
⊢ M.Parallel e✝ e✝