Type check requires id

Stream: general

[Patrick Johnson]

Why does the first example fail, but the second one works? I read somewhere that adding ids helps type-checking, but I don't understand what prevents the kernel to type-check it without the id in this case? Or is it a limitation of the elaborator?

constant F : ℕ → Prop

axiom h₁ : F 1
axiom h₂ : ∀ (P : Prop), F 0 → P
axiom h₃ : ∀ (P : ℕ → Prop) (n : ℕ), F n → P 1 → P n

def f : ℕ → ℕ
| (n + 2) := 0
| _ := 1

example {P : Prop} {n : ℕ} (h : F (n + 2)) : P :=
h₂ P (h₃ (λ x, F (f x)) (n + 2) h h₁)

example {P : Prop} {n : ℕ} (h : F (n + 2)) : P :=
h₂ P (id h₃ (λ x, F (f x)) (n + 2) h h₁)