rintro m ⟨hm1, hm2⟩
case h
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
⊢ ∀ (y : ℕ), (fun n => 0 < n ∧ p n) y → y = n + 1
case h.intro
p : ℕ → Prop
n : ℕ
hn1 : p (n + 1)
hn2 : ∀ (y : ℕ), (fun n => p (n + 1)) y → y = n
m : ℕ
hm1 : 0 < m
hm2 : p m
⊢ m = n + 1