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