case relExt r =>
  simp [Semiformula.eval_rel]; intro e h; simp [congr_arg (rel r) (funext h)]
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✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInR)
no goals