exact pair_indep
case inr.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x y : α
hI : autoParam ({x, y} ⊆ M.E) _auto✝
hne : {x, y}.encard ≠ ⊤
⊢ M.Indep {x, y}
no goals