proposition: Theorem reduce0_reducestar : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), canonical A0 eqA ltM p -> exists t : list (Term A n), reducestar Q p t.
proof: Proof. Proof using plusA os cs. intros Q p H. generalize (Reducef Q (mks p H)). intros H'; elim H'. simpl in |- *. intros x H'0; exists (s2p A A0 eqA n ltM x); try assumption. Qed.