- and ≡ λp:Bool. λq:Bool. p [Bool] (q [Bool]) false
- or ≡ λp:Bool. λq:Bool. p [Bool] true (q [Bool])
+ and ≡ λp:Bool. λq:Bool. p [Bool] q false
+ or ≡ λp:Bool. λq:Bool. p [Bool] true q
+
+ When I first wrote up these answers, I had put `(q [Bool])` where I now have just `q` in the body of `and` and `or`. On reflection,
+ this isn't necessary, because `q` is already a `Bool`. But as I learned by checking these answers with Pierce's evaluator, it's
+ also a mistake. What we want is a result whose type _is_ `Bool`, that is, `∀α. α -> α -> α`. `(q [Bool])` doesn't have that type, but
+ rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `∀`. The second, wrong type doesn't; it only has `∀`s
+ inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `∀`, since
+ `P -> ∀α. Q ≡ ∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.