refine ⟨fun h _ _ he hf ↦ pair_indep he hf, fun h ↦ ?_⟩
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}
⊢ M.Simple