proposition: Lemma PolZeq_correct : forall P P' l, PolZeq P P' = true -> PhiR l P == PhiR l P'.
proof: Proof. intros;apply (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext Rtheory));trivial. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia