proposition: Theorem not_nil_in_polySet : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), ~ inPolySet (pO A n) Q.
proof: Proof. intros Q H'; red in |- *; intros H'0. lapply (not_nil_in_polySet_elm Q (pO A n)); [ intros H'3; apply H'3 || elim H'3 | idtac ]; auto. Qed.