case step =>
  intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
  show x ^ step n₁' ≃ x ^ step n₂'
  have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
  calc
    _ ≃ x ^ step n₁' := Rel.refl
    _ ≃ x ^ n₁' * x  := pow_step
    _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
    _ ≃ x ^ step n₂' := Rel.symm pow_step
ℕ : 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₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ x ^ step m
no goals