proposition: Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv.
proof: Proof. unfold Pphi_dev;intros;apply Pphi_avoid_ok. - intros;apply mkpow_ok. - intros;apply mkopp_pow_ok. - intros;apply mkmult_pow_ok. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory