(subst
	(subst
		(subst
			(subst
				((| #f) #t)
				[
					(= (\m (\n ((& (<= m n)) (<= n m)))))
				]
			)
			[
				(<= (\m (\n (zero? ((- m) n)))))
			]
		)
		[
			(2 (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)))
		]
	)
	[(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))))))
	]
)