set r : ι → ι → Prop := WellOrderingRel
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
⊢ P univ
α : Type u_1
ι : Type u
M : Matroid α
P : Set ι → Prop
h_empty : P ∅
r : ι → ι → Prop := WellOrderingRel
⊢ P univ