funext x
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
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