theorem list_skip_index {α : Type u_1} (w : List α) (hw : w.length ≥ 2) (h_skip : ∀ (k : ℕ) (hk : k + 2 < w.length), w[k] = w[k + 2]) (i : ℕ) (hi : i < w.length) : w[i] = if i % 2 = 0 then w[0] else w[1]

A list whose entries are $2$-periodic ($w[k] = w[k+2]$ whenever both make sense) is determined by its first two entries: $w[i] = w[0]$ if $i$ even, $w[1]$ if $i$ odd.