proposition: Lemma app2_inv : forall (x y z t : mon n) (p : listA), (p ++ consA x nilA) ++ consA y nilA = consA z (consA t nilA) -> x = z /\ y = t.
proof: Proof. intros x y z t p; case p; simpl in |- *; auto. intros H'; injection H'; simpl in |- *; auto. intros a l; case l; simpl in |- *; auto. intros H'; discriminate H'. intros a0 l0; case l0; simpl in |- *; auto. intros H'; discriminate H'. intros a1 l1 H'; discriminate H'. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)