proposition: Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv.
proof: Proof. unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros; now rewrite ?local_mkpow_ok. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory