proposition: Lemma norm_subst_spec : forall l pe, MPcond lmp l -> PEeval l pe == (norm_subst pe)@l.
proof: Proof. intros;unfold norm_subst. unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory