proposition: Theorem Conf_inv1 : forall (Q : list (poly A0 eqA ltM)) (a b c : Term A n) (nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c) (p q r r1 s1 : list (Term A n)), Confluent Q (pX a p) (pX b q) (pX c r) -> reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b nZb p q) r1 -> reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a c nZc p r) s1 -> eqP A eqA n r1 s1.
proof: Proof. Proof using plusA cs. intros Q a b c nZb nZc p q r r1 s1 H'0 H'1 H'2; inversion_clear H'0. apply H. rewrite sp_rew with (1 := cs) (a := a) (b := b) (nZ2 := nZb); auto. rewrite sp_rew with (1 := cs) (a := a) (b := c) (nZ2 := nZc); auto. Qed.