simp_rw [unifOn_ground_eq, unifOn_erk_eq, min_le_iff, iff_true_intro rfl.le,
  or_true, true_and, simple_iff_forall_pair_indep, unifOn_ground_eq, unifOn_indep_iff,
  and_iff_right (encard_pair_le _ _)]
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E 2).E = E ∧ (unifOn E 2).erk ≤ 2 ∧ (unifOn E 2).Simple
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → {e, f} ⊆ E