proposition: Lemma not_nil_in_polySet_elm : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), inPolySet p Q -> p <> pO A n.
proof: Proof. intros Q p H'; elim H'; auto. intros a p0 H'0 H'1; red in |- *; intros H'2; inversion H'2. Qed.