Subst[body; old; new].

&Apply[];

&Apply[].
===
scm'((lambda (\x) \body) \arg)': Subst[\body; \x; \arg] &Subst[];
E[scm'(\x \y)']: scm'(\(E[\x]) \(E[\y]))';

&Subst[].
===
Subst[\old; \old; \new]: \new;
Subst[scm'(lambda (\old) \body)'; \old; \]: scm'(lambda (\old) \body)';
Subst[scm'(lambda (\x) \body)'; \old; \new]: scm'(lambda (\x) \(Subst[\body; \old; \new]))';
Subst[scm'(\f \x)'; \old; \new]: scm'(\(Subst[\f; \old; \new]) \(Subst[\x; \old; \new]))';
Subst[\body; \; \]: \body;
E[scm'(\x \y)']: scm'(\(E[\x]) \(E[\y]))';
E[scm'(lambda (\x) \body)']: scm'(lambda (\x) \(E[\body]))';