have h' := h.cl_eq_cl
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
⊢ M.Loop f
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {e} = M.cl {f}
⊢ M.Loop f