# Propositions and Proofs

Scripts from the third chapter of the book
## Exercises

- 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

## Errata

- 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.

Going home

Pierre Castéran