10. The Idea on One Page🔗

• An object-language binder becomes a Lean fun. Lean then does the scoping, renaming, and substitution work.

• Making the variable type a parameter, Term' v, keeps the datatype positive. Quantifying over it, ∀ v, Term' v, says that a term works for any representation of variables.

• The caveat: ∀ v alone does not prove, inside Lean, that a term treats every v the same way. When a theorem compares two interpretations, it needs the well-formedness hypothesis.

Every operation chooses the representation of variables that suits it:

• v := Unit forgets variable identity, to count occurrences.

• v := String gives printable names.

• v := Nat gives binder depths, and from them de Bruijn indices.

• v := Term' v₀ makes variables into syntax, which is substitution.

• v := Ty.denote makes variables into values, which is evaluation, and the setting for proofs about evaluation.