proposition: Lemma inPolySet_is_pX : forall (p : list (Term A n)) (L : list (poly A0 eqA ltM)), inPolySet p L -> exists a : Term A n, (exists q : list (Term A n), p = pX a q).
proof: Proof. intros p L H'; elim H'; auto. intros a p0 H'0 H'1; exists a; exists p0; auto. Qed.