3 Examples

1. Show that . We prove this using the abstraction rule, and noticing that the result is an instance of the projection rule.
   
   
2. As an example of an expression that is incorrectly typed, let's try to prove that .
   
   We get a contradiction that is of type implies that is of type .

3. Any free variables appearing in an expression to be typed must already be typed in the environment. For example,