have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
ℕ : 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₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
ℕ : 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₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
this : n₁' ≃ n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'