Exercise 4.2

\underbrace{\underbrace{\underbrace{trice}_{∀A:Set(A→A)→A→A} \underbrace{( \underbrace{trice}_{∀A:Set(A→A)→A→A}(A := nat))}_{(ℕ→ℕ→)→ℕ→ℕ}}_{A is implicit and set to ℕ: (ℕ → ℕ) → ℕ → ℕ} S}_{ℕ→ℕ} 0

ℕ