replace h := (cl_eq_loops_of_subset hX) ▸ h.basis_cl_right
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I X
⊢ I = ∅
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I (M.cl ∅)
⊢ I = ∅