constructor
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 ↔ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple
case mp
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 → M.E = E ∧ M.erk ≤ 2 ∧ M.Simple

case mpr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple → M = unifOn E 2