proposition: Theorem fP_app : forall p q : list (Term A n), fP (p ++ q) = fP p ++ fP q.
proof: Proof. intros p; elim p; simpl in |- *; auto. intros a l H' q. rewrite (H' q); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)