proposition: Theorem irreducible_eqp_com : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), irreducible Q p -> canonical A0 eqA ltM p -> eqP A eqA n p q -> irreducible Q q.
proof: Proof. Proof using plusA os cs. unfold irreducible in |- *. intros Q p q H' H'0 H'1 q0; red in |- *; intros H'2. apply H' with (q := q0); auto. apply reduce_eqp_com with (p := q) (q := q0); auto. apply eqp_imp_canonical with (1 := cs) (p := p); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.