Theorem: LO.FirstOrder.Semiterm.substs₂_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 σ
n' : ℕ
⊢ ∀ (a : Semiterm L μ n' × Semiterm L μ n'), Semiterm L μ 2 → encode [a.1, a.2] = encode ![a.1, a.2]
Tactic:
intro x _
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 σ
n' : ℕ
x : Semiterm L μ n' × Semiterm L μ n'
b✝ : Semiterm L μ 2
⊢ encode [x.1, x.2] = encode ![x.1, x.2]

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 σ
n' : ℕ
x : Semiterm L μ n' × Semiterm L μ n'
b✝ : Semiterm L μ 2
⊢ encode [x.1, x.2] = encode ![x.1, x.2]
Tactic:
simp[encode_finArrow]
State after:
no goals