Theorem: LO.FirstOrder.Semiterm.rewrite_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
⊢ Primrec₂ fun v p => (Rew.rewrite v) p
Tactic:
exact this.of_eq <| by intro v p; rfl
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
⊢ ∀ (a : Fin k → Semiterm L μ n) (b : Semiterm L (Fin k) n), (Rew.bind (fun x => #x) a) b = (Rew.rewrite a) b
Tactic:
intro v p
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
v : Fin k → Semiterm L μ n
p : Semiterm L (Fin k) n
⊢ (Rew.bind (fun x => #x) v) p = (Rew.rewrite v) p

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
v : Fin k → Semiterm L μ n
p : Semiterm L (Fin k) n
⊢ (Rew.bind (fun x => #x) v) p = (Rew.rewrite v) p
Tactic:
rfl
State after:
no goals