right
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ M.Nonloop f ∨ f = f
case h
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f✝ x : α
I C : Set α
he : M.Nonloop e
f : α
he' : (M.parallelExtend e f).Nonloop e
⊢ f = f