proposition: Lemma checker_nf_sound : forall (l : list NFormula) (cm : Psatz), check_normalised_formulas l cm = true -> forall env : PolEnv, make_impl (eval_nformula env) l False.
proof: Proof. intros l cm H env. unfold check_normalised_formulas in H. revert H. case_eq (eval_Psatz l cm) ; [|discriminate]. intros nf. intros H H0. rewrite <- make_conj_impl. intro H1. assert (H1' := make_conj_in _ _ H1). assert (Hnf := @eval_Psatz_Sound _ _ H1' _ _ H). destruct nf. apply (@check_inconsistent_sound _ _ H0 env Hnf). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl