simpa
case inl
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
⊢ M.Indep (if x ∈ {x} then insert e ({x} \ {x}) else {x}) ∧ (x = x ∨ x ∈ M.E) ↔ M.Nonloop x ∨ x = x
no goals