Subst[body; old; new].
AndMap[f; xs].
Apply[f; x].
IsEqual[x; y].
IsSymbol[].

&Curry[];
&Apply[];

&Curry[].
===
scm'(lambda (\x \x2 . \xs) \body)': scm'(lambda (\x) (lambda (\x2 . \xs) \body))';
scm'(\f \arg . \args)' &NonEmpty[xs: \args] &IsFalse[x: IsEqual[\f; scm'lambda']]: scm'((\f \arg) . \args)';
E[&Recurse[]];


&Apply[].
===
scm'((lambda (\x) \body) \arg)' &Env[]: 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; \] &Env[x: \old]: scm'(lambda (\old) \body)';
Subst[scm'(lambda (\x) \body)'; \old; \new] &Env[]: 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[&Recurse[]];

&Env[x; x2; xs].
---
\x: Scheme_Symbol[\];
Apply[IsSymbol[]; \x2] &Helpers[]: True[];
AndMap[IsSymbol[]; \xs] &Helpers[]: True[];
&NonEmpty[];

&IsTrue[x].
---
\x &Helpers[]: True[];

&IsFalse[x].
---
\x &Helpers[]: False[];

&NonEmpty[xs].
---
\xs: Scheme_Cons[\; \];

&Helpers[].
===
AndMap[\f; Scheme_Nil[]]: Scheme_Nil[];
AndMap[\f; Scheme_Cons[\x; \xs]] &IsTrue[x: Apply[\f; \x]]: AndMap[\f; \xs];
AndMap[\; Scheme_Cons[\; \]]: False[];
Apply[IsSymbol[]; Scheme_Symbol[\]]: True[];
Apply[IsSymbol[]; \]: False[];
IsEqual[\x; \x]: True[];
IsEqual[\; \]: False[];

&Recurse[].
---
E[scm'(\x \y)']: scm'(\(E[\x]) \(E[\y]))';
E[scm'(lambda (\x) \body)']: scm'(lambda (\x) \(E[\body]))';