Theorem: LO.FirstOrder.Completeness.Model.val (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
n : ℕ
e : Fin n → SyntacticTerm L
ε : ℕ → Model T Γ
t : SyntacticSemiterm L n
⊢ Semiterm.val (structure T Γ) e ε t = (Rew.bind e ε) t
Tactic:
induction t <;> simp[*, Semiterm.val_func, Rew.func]
State after:
case func
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
n : ℕ
e : Fin n → SyntacticTerm L
ε : ℕ → Model T Γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ℕ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.val (structure T Γ) e ε (a✝ a) = (Rew.bind e ε) (a✝ a)
⊢ (Structure.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)) = Semiterm.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)

State before:
case func
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
n : ℕ
e : Fin n → SyntacticTerm L
ε : ℕ → Model T Γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ℕ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.val (structure T Γ) e ε (a✝ a) = (Rew.bind e ε) (a✝ a)
⊢ (Structure.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)) = Semiterm.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)
Tactic:
rfl
State after:
no goals