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 47, Definition 8, "A goal is the pairing ... and a type P that
is well-formed ..."
"a proof of P that should be a well-formed term t of type P in the environment
- 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.