proposition: Lemma eval_Psatz_sound : forall env w l f', make_conj (eval_nformula env) l -> eval_Psatz l w = Some f' -> eval_nformula env f'.
proof: Proof. intros env w l f' H H0. apply (fun H => eval_Psatz_Sound Zsor ZSORaddon l _ H w) ; auto. apply make_conj_in ; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat