for U being non empty set
for S being Language
for l being literal Element of S
for phi0 being 0wff string of S
for I being b₂,b₁ -interpreter-like Function
for tt being Element of AllTermsOf S holds I -AtomicEval ((l,tt) AtomicSubst phi0) = ((l,((I -TermEval) . tt)) ReassignIn I) -AtomicEval phi0