proposition: Lemma pick_inv_eqT : forall (Q : list (poly A0 eqA ltM)) (a b : Term A n) (p q : list (Term A n)), pickinSetp a (pX b q) Q -> divP A A0 eqA multA divA n a b.
proof: Proof. intros Q a b H' q H'0. apply pick_inv_eqT_lem with (Q := Q) (p := pX b q) (q := q); auto. Qed.