Propositions and Proofs

Exercises

1. Exercises 3.2 page 58 and 3.3 page 65
2. Exercise 3.4 page 67
3. Exercise 3.5 page 69
4. Exercise 3.6 page 71

Errata

1. Page 21, in the Var rule, read (x:A) instead of
2. Page 52, same correction.
3. Page 63 (last paragraph): read "Calling "apply H0" generates three subgoals: P->Q->R, R and T->Q" Please replace intro H2 with intro H1 and H1 with H0, to be OK with the proof script.
4. Page 70 (last paragraph): read "forall P Q R: Prop"