# formal proof – Show by induction hypothesis in the typing structure in \$lambda\$-calculus

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.