+
(**************************************************************************)
(* __ *)
(* ||M|| *)
intros.elim n.
simplify.reflexivity.
simplify.
-demodulate all steps=3.
+demodulate all.
(*
apply eq_f.rewrite < H.
transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
intros.elim x.
simplify.reflexivity.
simplify.
-demodulate all steps=16.
+demodulate all.
(*
rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
intros.
elim x. simplify.apply refl_eq.
simplify.
-demodulate all steps=4.
+demodulate all.
(*
rewrite < sym_times.
rewrite > distr_times_plus.