proposition: Theorem incl_addEnd1 : forall (a : poly A0 eqA ltM) (L1 L2 : list (poly A0 eqA ltM)), incl (addEnd A A0 eqA n ltM a L1) L2 -> incl (a :: L1) L2.
proof: Proof. unfold incl in |- *; simpl in |- *; auto. intros a L1 L2 H' a0 H'0; case H'0; [ intros H'1; rewrite <- H'1; clear H'0 | intros H'1; clear H'0 ]; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)