(forall (a b) (* a (succ b)) (+ a (* a b)))
(forall (a)   (* a 0) 0)