Theorem: LO.FirstOrder.Semiterm.val_operator (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s e ε (o.operator v) = o.val fun x => val s e ε (v x)
Tactic:
simp [Operator.operator, val_substs]
State after:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s (fun x => val s e ε (v x)) (fun a => instIsEmptyEmpty.elim a) o.term = o.val fun x => val s e ε (v x)

State before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s (fun x => val s e ε (v x)) (fun a => instIsEmptyEmpty.elim a) o.term = o.val fun x => val s e ε (v x)
Tactic:
congr
State after:
case e_ε
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ (fun a => instIsEmptyEmpty.elim a) = Empty.elim

State before:
case e_ε
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ (fun a => instIsEmptyEmpty.elim a) = Empty.elim
Tactic:
funext x
State after:
case e_ε.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
x : Empty
⊢ instIsEmptyEmpty.elim x = x.elim

State before:
case e_ε.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
x : Empty
⊢ instIsEmptyEmpty.elim x = x.elim
Tactic:
contradiction
State after:
no goals