rwa [h0, h0] at x_ih
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
h : f (x + 1) ≤ x
x_ih : f (f (f (x + 1))) = f (f (x + 1))
⊢ f (x + 1) = x + 1
no goals