apply ind_on (motive := λ n => step n ≄ n) n
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step n ≄ n
case zero
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ step 0 ≄ 0

case step
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m