proposition: Theorem Opm_ind : forall (P : list (Term A n) -> list (Term A n) -> Prop) (p q : list (Term A n)), (forall p : list (Term A n), P (pO A n) p) -> (forall p : list (Term A n), P p (pO A n)) -> (forall (a b : Term A n) (p q : list (Term A n)), P (pX a p) q -> ltT ltM a b -> P (pX a p) (pX b q)) -> (forall (a b : Term A n) (p q : list (Term A n)), P p (pX b q) -> ltT ltM b a -> P (pX a p) (pX b q)) -> (forall (a b : Term A n) (p q : list (Term A n)), P p q -> eqT a b -> P (pX a p) (pX b q)) -> forall p q : list (Term A n), P p q.
proof: Proof. Proof using ltM_dec. intros P H' H'0 H'1 H'2 H'3 H'4 H'5 p; elim p; auto. intros a l H'6 q; elim q; auto. intros a0 l0 H'7; (case (ltT_dec A n ltM ltM_dec a a0); [ intros temp; case temp; clear temp | idtac ]; intros test); change (P (pX a l) (pX a0 l0)) in |- *; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)