proposition: Theorem confl_reducestar : forall Q : list (poly A0 eqA ltM), SpolyQ Q -> forall p : list (Term A n), canonical A0 eqA ltM p -> ReduStarConfluent Q p.
proof: Proof. Proof using plusA os cs. intros Q H' p H'0. generalize (confl_restar Q H' (mks A A0 eqA n ltM p H'0)); simpl in |- *; auto. Qed.