rintro ⟨h, rfl⟩
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)
case inl.refine_2.intro
α : Type u_1
M' : Matroid α
e f : α
I : Set α
he' : e ∉ M'.E
h : M'.Loop e
he : e ∉ (M' ＼ e).E
⊢ False