proposition: Theorem Incl_inp_inPolySet : forall P Q : list (poly A0 eqA ltM), incl P Q -> forall p : list (Term A n), inPolySet p P -> inPolySet p Q.
proof: Proof. intros P Q H' p H'0; auto. elim (inPolySet_inv1 P p); [ intros q E; elim E; intros H'4 H'5; clear E | idtac ]; auto. rewrite H'5. apply in_inPolySet; auto. rewrite <- H'5; auto. apply inPolySet_inv0 with (P := P); auto. Qed.