Added shifting and substitution to Syntax
Context does shifting, can lookup hints
Added alpha-equivalence to Syntax
Added term normalization function to Typing
Added missing magenta annotations to Syntax