proposition: Theorem reduce_inv : forall (Q : list (poly A0 eqA ltM)) (a b : Term A n) (p q : list (Term A n)), reduce Q (pX a p) (pX b q) -> eqTerm (A:=A) eqA (n:=n) a b -> canonical A0 eqA ltM (pX a p) -> reduce Q p q.
proof: Proof. Proof using plusA os cs. intros Q a b p q H'; inversion_clear H'; auto. intros eq Cap. elim (not_double_canonical A A0 eqA n ltM) with (a := b) (p := q); auto. apply eqp_imp_canonical with (p := pX b (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b0 nZb p q0)) (1 := cs); auto. apply (canonical_pX_eqT A A0 eqA n ltM) with (a := a); auto. apply canonical_spminusf_full_t with (1 := cs); auto. apply inPolySet_imp_canonical with (L := Q); auto. apply (eqTerm_imp_eqT A eqA n); auto. apply nzeroP_comp_eqTerm with (1 := cs) (a := a); auto. apply canonical_nzeroP with (p := p) (ltM := ltM); auto. Qed.