proposition: Theorem inPolySet_inv1 : forall (P : list (poly A0 eqA ltM)) (p : list (Term A n)), inPolySet p P -> exists q : poly A0 eqA ltM, In q P /\ p = s2p q.
proof: Proof. intros P p H'; elim H'; auto. intros a p0 H P0. exists (exist (canonical A0 eqA ltM) (a :: p0) H); split; simpl in |- *; auto. intros a p0 P0 H'0 H'1; elim H'1; intros q E; elim E; intros H'2 H'3; clear E H'1. exists q; split; simpl in |- *; auto. Qed.