Propositions and Proofs
Scripts from the third chapter of the book
- Exercises 3.2 page 58 and 3.3 page 65
- Exercise 3.4 page 67
- Exercise 3.5 page 69
- Exercise 3.6 page 71
- Page 21, in the Var rule, read (x:A) instead of
- Page 52, same correction.
- 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.
- Page 70 (last paragraph): read "forall P Q R: Prop"