case step =>
  intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
  show x ^ 0 ≃ x ^ step n₂'
  exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_zero)
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ x ^ step m
no goals