I’m starting to study lambda calculus and I need help with the proof methods, especially with induction over typing.
For example, on the
Lemma (Weakening) If $Gammavdash t:T$ and $xnotin dom(Gamma)$, then $Gamma,x:Svdash t:T$. Moreover, the latter derivation has the same depth as the former.
I only need tools or explanations about this type of demonstration, and for me to practice.
I think the ways to show are: by derivation in typing, by the last rule used. But I am not understanding how to use it.
Note: I use the book Type Systems for Programming Languages by Pierce.