-(* some problem here: confusion between relations/symmetric
-and functions/symmetric; functions symmetric is not in
-functions.moo why?
-theorem symmetric_plus: symmetric nat plus. *)
-
-theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).