∀ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {x v w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α],
  G.IsFiveWheelLike r k v w₁ w₂ s t →
    G.CliqueFree (r + 2) →
      ∀ [inst_1 : DecidableRel G.Adj],
        (∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y) →
          {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}.card ≤ 2 →
            ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))