(infer (sum 0 X X))
(infer (sum (s X) Y (s Z)) from (sum X Y Z))

(infer? (print (part 1 a)))
  (infer? (sum 0 0 0))

(infer? (print (part 1 b)))
  (infer? (sum (s (s 0)) (s (s (s 0))) W) (print (answer: W)))

(infer? (print (part 1 c)))
  (infer? (sum (s (s 0)) D (s (s (s (s (s 0)))))) (print (answer: D)))


(infer (prod 0 X 0) from (print (prod-base X)))
(infer (prod (s X) Y Z)
  from (print (prod-ind X Y Z))
	  (prod X Y W) (print (prod-W= W)) (sum  Y W Z))


(infer? (print (part 2 a)))
  (infer? (prod 0 0 0))

(infer? (print (part 2 b)))
  (infer? (prod (s (s 0)) (s (s (s 0))) W) (print (answer: W)))

(infer? (print (part 2 c)))
  (infer? (prod (s (s 0)) D (s (s (s (s (s (s 0))))))) (print (answer: D)))