Set: pp::colors
  Set: pp::unicode
λ (A : Type) (a : A), let b := a in b : Π (A : Type), A → A
  Assumed: g
  Defined: f
f ℕ 10
f ℤ (- 10)