English
Let α be a type with a denumerable structure. For any v ∈ ℕ, if v is written as a pair (v1, v2) via unpair, then the encoding of the nonempty list whose head is the encoding of v1 and whose tail is the encoding of the list at index v2 equals succ v. In particular, the encoding of the nonempty list corresponding to v encodes to v+1 as a head-tail construction.
Русский
Пусть α — тип с денумерабельной структурой. Пусть v ∈ ℕ и разложим v на пару (v1, v2) с помощью разложения unpair. Тогда кодирование не-пуского списка с головой, кодирующейся как ofNat α v1, и хвостом, кодирующимся как ofNat (List α) v2, равно succ v. Конкретнее: если unpair v = (v1, v2), то ofNat (List α) (succ v) = ofNat α v1 :: ofNat (List α) v2.
LaTeX
$$$\\displaystyle \\text{If }\\text{unpair}(v)=(v_1,v_2),\\quad \\operatorname{ofNat}(\\text{List } \\alpha)(\\operatorname{succ} v)=\\operatorname{ofNat} \\alpha\\bigl(v_1\\bigr)\\;::\\;\\operatorname{ofNat}(\\text{List } \\alpha)(v_2).$$$
Lean4
@[simp, nolint unusedHavesSuffices] -- This is a false positive in the unusedHavesSuffices linter.
theorem list_ofNat_succ (v : ℕ) : ofNat (List α) (succ v) = ofNat α v.unpair.1 :: ofNat (List α) v.unpair.2 :=
ofNat_of_decode <|
show decodeList (succ v) = _ by
rcases e : unpair v with ⟨v₁, v₂⟩
simp [decodeList, e]
rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some]
