obtain (he' | he') := em' (e ∈ M'.E)
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
case inl
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M

case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M