case step =>
  intro n (ih : step n ≄ n)
  show step (step n) ≄ step n
  intro (_ : step (step n) ≃ step n)
  show False
  apply ih
  show step n ≃ n
  exact AA.inject ‹step (step n) ≃ step n›
ℕ : Type
inst✝¹ : Core ℕ
inst✝ : Induction ℕ
n : ℕ
⊢ ∀ (m : ℕ), step m ≄ m → step (step m) ≄ step m
no goals