(subst
	(subst
		((- 1) 2)
		[
			(2 (succ 1))
			(+ (\m(\n ((m succ) n))))
			(* (\m(\n(\f (m (n f))))))
			(** (\b(\e (e b))))
			(- (\m(\n ((n pred) m))))
		]
	)
	[(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))
	 )
	]
)