simp [Parallel, h]
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x✝ : M.Loopless ∧ M.parallelClasses = Partition.discrete {e | M.Nonloop e}
left✝ : M.Loopless
h : M.parallelClasses = Partition.discrete {e | M.Nonloop e}
⊢ ∀ (e f : α), M.Parallel e f → e = f
no goals