intro a
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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subtEquiv (t z))
⊢ ∀ (n : α),
    encode
        (UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b n ⟨x, hx⟩)) else default)
          (fun x => ↑(subtEquiv (e n x))) ↑(subtEquiv (t n))) =
      encode ((Rew.bind (b n) (e n)) (t n))
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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subtEquiv (t z))
a : α
⊢ encode
      (UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e a x)))
        ↑(subtEquiv (t a))) =
    encode ((Rew.bind (b a) (e a)) (t a))