exact h
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
H :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s (fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) Empty.elim) (ι.rel r)
no goals