Just to give the proof as a whole in this notation for others, assume (→) has lower precedence than (∨) and is right-associative (i.e. that a → b → c = a → (b → c)):

  Proving: (p ∨ q → p ∨ r) → p ∨ (q → r)
  Start from:
    (x → y) → (y → z) → x → z
  Replace x with q, y with p ∨ q, z with p ∨ r:
    (q → p ∨ q) → (p ∨ q → p ∨ r) → q → p ∨ r
  The first part (q → p ∨ q) is already a known tautology so via modus ponens
    (p ∨ q → p ∨ r) → q → p ∨ r
  Replace the last → with its definition, (a → b) = ¬a ∨ b:
    (p ∨ q → p ∨ r) → ¬q ∨ p ∨ r
  Use the commutative property of (∨):
    (p ∨ q → p ∨ r) → p ∨ ¬q ∨ r
  Then use the definition again:
    (p ∨ q → p ∨ r) → p ∨ (q → r)
  QED.

The first part is also valid in intuitionistic logic and essentially just transforms a known truth `x → y` into "continuation passing style" `∀z. (y → z) → x → z` with a valid result, I think this is why the authors were quite pleased with the proof.

The second half is the shifty bit for intuitionistic logic, going from `q -> Either p r` to `Either p (q -> r)` where it's really easy to see that you could not, say, have a Haskell function of that type generally.