Formal target: Corpus.OEIS108081.count_words_in_x_is_a_shifted

"The number of words of length $n$ for $n \le 12$ is given by $a(n+1)$.

Exact formal statement

∀ (n : Nat),
  GE.ge.{0} n 1 → Eq.{1} (Set.ncard.{0} (Corpus.OEIS108081.xN n)) (Corpus.OEIS108081.a (HSub.hSub.{0, 0, 0} n 1))

This target is a formal statement, not a proof of the problem.

Environment availability: available.