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