congr
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
    func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
case funcExt.e_a
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) = fun i =>
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)