refine iff_of_false ?_ ?_
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 inl.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬M' = M.addLoop e

case inl.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬(M'.Loop e ∧ M' ＼ e = M)