definition f : ℕ → ℕ :=
λ a, a + 1
definition f [reducible] : ℕ → ℕ :=
λ a, a + 1
definition f : ℕ → ℕ :=
λ a, a + 1
definition f [reducible] : ℕ → ℕ :=
λ a, a + 1