proposition: Theorem in_inPolySet : forall (P : list (poly A0 eqA ltM)) (p : poly A0 eqA ltM), In p P -> ~ eqP A eqA n (s2p p) (pO A n) -> inPolySet (s2p p) P.
proof: Proof. intros P; elim P; auto. intros p H'; inversion H'. simpl in |- *. intros a l H' p H'0; elim H'0; [ intros H'1; rewrite <- H'1; clear H'0 | intros H'1; clear H'0 ]; auto. case a; simpl in |- *. intros x; case x; auto. intros c H'0; elim H'0; auto. intros t l0 c H; change (inPolySet (pX t l0) (exist (canonical A0 eqA ltM) (pX t l0) c :: l)) in |- *; apply incons. Qed.