Product of list


Definition

 prod_list.Nil: prod_list [] = 1
prod_list.Cons: prod_list (?x # ?xs) = ?x * prod_list ?xs
THEOREM    prod_list (xs @ ys) = prod_list xs * prod_list ys
prod_list.append:
	prod_list (?xs @ ?ys) = prod_list ?xs * prod_list ?ys

Proof unavailable