proposition: Lemma pick_inv_eqT_lem : forall (Q : list (poly A0 eqA ltM)) (a : Term A n) (p : list (Term A n)), pickinSetp a p Q -> forall (b : Term A n) (q : list (Term A n)), p = pX b q -> divP A A0 eqA multA divA n a b.
proof: Proof. intros Q a p H'; elim H'; auto. intros a0 b p0 H'0 H'1 H'2 b0 q H'3; injection H'3; auto. intros H'4 H'5; rewrite <- H'5; auto. Qed.