proposition: Theorem ltP_refl_pX : forall (a : Term A n) (p : list (Term A n)), canonical A0 eqA ltM (pX a p) -> ltP (A:=A) (n:=n) ltM p (pX a p).
proof: Proof. Proof using plusA os multA minusA invA divA cs A1. intros a p; case p; auto. intros a0 l H'. apply ltP_trans with (y := pX a (pO A n)); auto. change (ltP (A:=A) (n:=n) ltM (pX a0 l) (pX a (pO A n))) in |- *. apply ltP_hd; auto. apply (canonical_pX_order A A0) with (eqA := eqA) (l := l); auto. apply ltP_tl; auto. change (ltP (A:=A) (n:=n) ltM (pO A n) (pX a0 l)) in |- *; apply ltPO. Qed.
imports: Coq(Arith Compare_dec)