rwa [parallel_self_iff]
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
he' hf : (M.parallelExtend e e).Nonloop e
⊢ (M.parallelExtend e e).Parallel e e
no goals