proposition: Theorem imp_in : forall (P : list (poly A0 eqA ltM)) (a : list (Term A n)), inPolySet A A0 eqA n ltM a P -> exists b : poly A0 eqA ltM, In b P /\ a = s2p A A0 eqA n ltM b.
proof: Proof. intros P a H'; elim H'; auto. intros a0 p H P0; exists (exist (fun l0 : list (Term A n) => canonical A0 eqA ltM l0) (pX a0 p) H); split; auto. simpl in |- *; auto. intros a0 p P0 H'0 H'1; elim H'1; intros b E; elim E; intros H'2 H'3; clear E H'1; auto. exists b; split; auto with datatypes. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)