proposition: Theorem uniq_minusp : forall (l : list (Term A n) * list (Term A n)) (l3 l4 : list (Term A n)), minusP (fst l) (snd l) l3 -> minusP (fst l) (snd l) l4 -> l3 = l4.
proof: Proof. Proof using os. unfold pX, pX in |- *. intros l; pattern l in |- *. apply well_founded_ind with (1 := wf_lessP A n). intros (l1, l2); simpl in |- *. case l1; clear l1. intros H' l3 l4 H'0; inversion_clear H'0; intros H'2; inversion_clear H'2; auto. case l2; clear l2. simpl in |- *; intros n0 l0 H' l3 l4 H'0 H'2. inversion H'2; inversion H'0; auto. simpl in |- *; intros n2 l2 n1 l1 Induc l3 l4 Hl3 Hl4. case (minusP_inv l1 l2 l4 n1 n2); auto. intros x H'; elim H'; intros H'0; [ idtac | elim H'0; clear H'0; intros H'0 ]; clear H'; (case (minusP_inv l1 l2 l3 n1 n2); auto; intros x1 H'; elim H'; intros H'1; [ idtac | elim H'1; clear H'1; intros H'1 ]; clear H'). elim H'1; intros H' H'2; elim H'2; intros H'3 H'4; rewrite H'4; clear H'2 H'1. elim H'0; intros H'1 H'2; elim H'2; intros H'5 H'6; rewrite H'6; clear H'2 H'0. apply pX_inj; auto. apply Induc with (y := (l1, pX n2 l2)); auto. red in |- *; red in |- *; simpl in |- *; auto. elim H'1; intros H' H'2; clear H'1. elim H'0; intros H'1 H'3; clear H'0. absurd (ltT ltM n1 n2); auto. elim H'1; intros H' H'2; clear H'1. elim H'0; intros H'1 H'3; clear H'0. absurd (eqT n2 n1); auto. apply (eqT_sym A n); auto. elim H'1; intros H' H'2; clear H'1. elim H'0; intros H'1 H'3; clear H'0. absurd (ltT ltM n1 n2); auto. elim H'1; intros H' H'2; elim H'2; intros H'3 H'4; rewrite H'4; clear H'2 H'1. elim H'0; intros H'1 H'2; elim H'2; intros H'5 H'6; rewrite H'6; clear H'2 H'0. apply pX_inj; auto. apply Induc with (y := (pX n1 l1, l2)); auto; red in |- *; simpl in |- *; auto. rewrite <- plus_n_Sm; auto. elim H'1; intros H' H'2; clear H'1. elim H'0; intros H'1 H'3; clear H'0. absurd (eqT n1 n2); auto. elim H'1; intros H' H'2; clear H'1. elim H'0; intros H'1 H'3; clear H'0. absurd (eqT n2 n1); auto. apply (eqT_sym A n); auto. elim H'1; intros H' H'2; clear H'1. elim H'0; intros H'1 H'3; clear H'0. absurd (eqT n1 n2); auto. elim H'1; intros H' H'2; elim H'2; [ intros H'3; clear H'2 H'1 | intros H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7; rewrite H'7; clear H'5 H'3 H'2 H'1 ]. elim H'0; intros H'1 H'2; elim H'2; [ intros H'4; clear H'2 H'0 | intros H'4; elim H'4; intros H'5 H'6; apply H'5 || elim H'5; try assumption; clear H'4 H'2 H'0 ]. elim H'4; intros H'0 H'2; clear H'4. elim H'3; intros H'4 H'5; clear H'3. apply Induc with (y := (l1, l2)); auto. red in |- *; red in |- *; simpl in |- *; rewrite <- plus_n_Sm; auto. elim H'3; intros H'0 H'2; clear H'3; auto. elim H'0; intros H'1 H'2; elim H'2; [ intros H'3; clear H'2 H'0 | intros H'3; elim H'3; intros H'5 H'8; elim H'8; intros H'9 H'10; rewrite H'10; clear H'8 H'3 H'2 H'0 ]. elim H'3; intros H'0 H'2; clear H'3. apply H'4 || elim H'4; auto. apply pX_inj; auto. apply Induc with (y := (l1, l2)); auto. red in |- *; red in |- *; simpl in |- *; rewrite <- plus_n_Sm; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)