unfolding from cases

Stream: general

[Reid Barton]

def x : ℕ := 1 + 1 + 1 + 1

inductive P : ℕ → Type
| p : P x

example {a} (h : P a) : a = 4 := begin
  cases h,
end

Goal is ⊢ nat.succ (nat.add (1 + 1 + 1) 0) = 4. Is all this unfolding expected? I wanted x = 4.

[Kenny Lau]

interestingly induction h produces the expected x = 0:

def x : ℕ := 0

inductive P : ℕ → Type
| p : P x

example {a} (h : P a) : a = 0 := begin
  induction h,
end