proposition: Theorem reducestar_eqp_com : forall (Q : list (poly A0 eqA ltM)) (p q r s : list (Term A n)), reducestar Q p q -> canonical A0 eqA ltM p -> eqP A eqA n p r -> eqP A eqA n q s -> reducestar Q r s.
proof: Proof. Proof using plusA os cs. intros Q p q r s H' H'0 H'1 H'2; inversion H'. apply reducestar0; auto. apply reduceplus_eqp_com with (p := p) (q := q) (1 := cs); auto. apply irreducible_eqp_com with (p := q) (1 := cs); auto. apply canonical_reduceplus with (1 := cs) (3 := H); auto. Qed.