proposition: Theorem reducestar_pO_is_pO : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), canonical A0 eqA ltM p -> reducestar Q (pO A n) (pO A n).
proof: Proof. intros Q p H' H'0; auto. apply reducestar0; auto. apply Rstar_0; auto. apply pO_irreducible. Qed.