Theorem·T39
Substitution into a term exists and is unique
The recursive substitution characterization genuinely determines exactly one term, for every term substituted into.
In words
For any term substituted into, its substitution result exists and is unique.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1By strong induction on : assume every term of length has existing uniquely (the induction hypothesis, "IH"); show the same for of length .
- 2By T32 (ii), is either for a unique , or for a unique - never both.
- 3Variable case. If : exactly one of or holds (trichotomy-style case split on equality). If , the match clause of D097 forces , a specific term; if , the other clause forces , a specific term. The two clauses never both apply (their hypotheses are exclusive), and by uniqueness of (T32 (ii)) this is the only term consistent with whichever clause applies. Existence and uniqueness hold.
- 4Function case. If with unique and : each for , by the same length bookkeeping as in the proof of T31. By the IH, exists uniquely for every , so is a genuine function (D018), and is a specific term (T30, D075). The func clause of D097 forces to equal it; by mutual exclusivity and uniqueness of , this is the only term consistent with D097.
- 5T08 concludes: exists and is unique for every .
∎
Remarks
Confirms the notation
is well posed for every term. The proof is exactly the same strong-induction-on-length shape used for term values and term variables, again licensed by unique readability.