no goals
L : Language
L' : Language
M : Type w
N : Type ?u.235577
P : Type ?u.235580
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
k : ℕ
R : Relations L k
ts : Fin k → Term L α
⊢ (RelMap R fun i => Term.realize (Sum.elim v default) (Term.relabel Sum.inl (ts i))) ↔
    RelMap R fun i => Term.realize v (ts i)
simp