Exercise 4.7
(a) Give λω-definitions of the notions legal term, statement, λω-context and domain.
(b) Formulate the following theorems for λω: Free Variables Lemma, Thinning Lemma, Substitution Lemma.
(a) The following are λω analogues of already defined notions.
A term $Γ ⊢ M:σ$ is legal in λω if there exists a context $Γ$ such that a term $M$ with type $σ$ is derivable, where $σ$ is a constructor (type or proper constructor), kind or $\Box$.
A statement is of the form $M:σ$ where $M$ is a term and $σ$ is a constructor, kind or $\Box$.
A λω-context is a list of declarations, where declarations are statements with a variable as the subject, and where the context is derivable according to the derivation rules.
A domain is the ordered list of subjects of the declarations in a context.
(b) The following are λω analogues of already defined theorems.
Free Variables Lemma. In a judgement $Γ⊢M:σ$, the free variables of $M$ are in the domain, that is, $FV(M) \subseteq dom(Γ)$.
Thinning Lemma. Let $Γ'$ and $Γ''$ be contexts such that $Γ' ⊆Γ''$. If $Γ' ⊢M : σ$, then also $Γ'' ⊢M : σ$.
Substitution Lemma. Assume $Γ', x : σ$, $Γ'' ⊢ M : τ$ and $Γ' ⊢N : σ$. Then $Γ', Γ'' ⊢M[x := N] : τ$.
Here, $σ$ is a constructor (type or proper constructor), kind or $\Box$.
