
diff git a/week2.mdwn b/week2.mdwn
index 6f157990..1cabf646 100644
 a/week2.mdwn
+++ b/week2.mdwn
@@ 3,21 +3,15 @@ Syntactic equality, reduction, convertibility
Define T to be `(\x. x y) z`. Then T and `(\x. x y) z` are syntactically equal, and we're counting them as syntactically equal to `(\z. z y) z` as well, which we will write as:
T ≡ `(\x. x y) z` ≡ `(\z. z y) z`

+> T ≡ `(\x. x y) z` ≡ `(\z. z y) z`
This:
T ~~> `z y`

+ T ~~> z y
means that T betareduces to `z y`. This:
M <~~> T

+ M <~~> T
means that M and T are betaconvertible, that is, that there's something they both reduce to in zero or more steps.
@@ 98,7 +92,9 @@ This question highlights that there are different choices to make about how eval
> \x. M x
> where x does not occur free in `M`, to `M`? It should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when etareduction is added to the proof theory is importantly different from the one where only betareduction is permitted.
+> where x does not occur free in `M`, to `M`?
+
+With regard to Q3, it should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when etareduction is added to the proof theory is importantly different from the one where only betareduction is permitted.
MORE on extensionality
@@ 130,7 +126,7 @@ Its syntax has the following tree:
/ \ / \
A B C D
Applicative order evaluation does what's called a "postorder traversal" of the tree: that is, we always go left and down whenever we can, and we process a node only after processing all its children. So `(C D)` gets processed before `((A B) (C D))` does, and `(E F)` gets processed before `((A B) (C D)) (E F)` does.
+Applicative order evaluation does what's called a "postorder traversal" of the tree: that is, we always go down when we can, first to the left, and we process a node only after processing all its children. So `(C D)` gets processed before `((A B) (C D))` does, and `(E F)` gets processed before `((A B) (C D)) (E F)` does.
Normal order evaluation, on the other hand, will substitute the expresion `(C D)` into the abstract that `(A B)` evaluates to, without first trying to compute what `(C D)` evaluates to. That computation may be done later.