(subst
	(subst
		(subst
			(subst
				((Y (\fac (\n (if (= n 0) 1 (* n (if (<= 2 n) (fac (- n 1)) 1)))))) (+ 0 3))
				[(= (\m (\n (& (<= m n) (<= n m)))))
				 (65 (+ 1 (* 4 (* 4 4))))])
			[(<= (\m (\n (zero? (- m n)))))])
		[(2 (succ 1))
		 (3 (succ (succ 1)))
		 (4 (succ (succ (succ 1))))
		 (+ (\m(\n (m succ n))))
		 (* (\m(\n(\f (m (n f))))))
		 (** (\b(\e (e b))))
		 (- (\m(\n (n pred m))))
		 (zero? (\n ((n (\x #f)) #t)))
		 (cons  (\x (\y (\s ((s x) y)))))
		 (nil   (\x #t))
		 (nil?  (\p (p (\x (\y #f)))))
		 (head  (\p (p #t)))
		 (tail  (\p (p #f)))
		 ])
	[(succ  (\n(\f(\x (f (n f x))))))
	 (pred  (\n(\f(\x(((n (\g(\h(h (g f))))) (\u x)) (\u u))))))
	 (1     (\ff(\xx (ff xx))))
	 (0     (\ff(\xx xx)))
	 (#t    (\x(\y x)))
	 (#f    (\x(\y y)))
	 (&     (\p(\q (p q p))))
	 (|     (\p(\q (p p q))))
	 (if    (\p(\a(\b (p a b)))))
	 (I     (\x x))
	 (K     (\x (\y x)))
	 (S     (\x (\y (\z ((x z) (y z))))))
	 (Y     (\f ((\x (f (x x))) (\x (f (x x))))))
	 (AY    (\f ((\x (f (\arg ((x x) arg)))) (\x (f (\arg ((x x) arg)))))))])