proposition: Theorem olist_X : forall (l : list _) a, olist (pX a l) -> olist l.
proof: Proof. intros l a H'. elim (dist_Desc_concat _ ltM (consA (T2M a) nilA) (fP l)); [ intros H'5 H'6 | idtac ]; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)