have rec_subst
  : (x : ℚ) → [AP (x ≄ 0)] → ctx.rec_diff a₁ x ≃ ctx.rec_diff a₂ x
  := this
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Integer.Induction ℤ
ℚ : Type
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂
⊢ p ^ a₁ ≃ p ^ a₂
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Integer.Induction ℤ
ℚ : Type
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂
rec_subst : ∀ (x : ℚ) [inst : AP (x ≄ 0)], ctx.rec_diff a₁ x ≃ ctx.rec_diff a₂ x
⊢ p ^ a₁ ≃ p ^ a₂