rw [or_iff_not_imp_left]
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : F₀ ⩿[M] F₁
⊢ F₀ = F₁ ∨ (F₀ ⋖[M] F₁)
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : F₀ ⩿[M] F₁
⊢ ¬F₀ = F₁ → F₀ ⋖[M] F₁