∀ {α : Type u} {σ : Type v} (M : DFA α σ) [inst : Fintype σ] {x : List α},
  x ∈ M.accepts →
    Fintype.card σ ≤ x.length →
      ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts