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