Substitution and Denotation

Proves that bound-variable operations commute with denotation.

• substK_denote — generalized depth-k substitution commutes with denote
• subst_denote / varOpen_denote — substitution and variable opening commute with denote
• liftBVars_denote — lifting bound variable indices preserves denotation
• substFvarsLifting_denote — free variable substitution with lifting commutes with denote

Generalized substK_denote

liftBVars and denotation

denoteArgs indexing

withArgs lemmas

Free-variable substitution commutes with denotation

substFvars denotation (via locally closed replacements)