proposition: Lemma agree_env_eval_nformulae : forall env env' l (AGREE : agree_env (max_var_nformulae l) env env'), make_conj (eval_nformula env) l <-> make_conj (eval_nformula env') l.
proof: Proof. intros env env' l; induction l as [|a l IHl]. - simpl. tauto. - intros. rewrite ! make_conj_cons. assert (eval_nformula env a <-> eval_nformula env' a) as H. { apply agree_env_eval_nformula. eapply agree_env_subset ; eauto. unfold max_var_nformulae. simpl. rewrite Pos.max_1_l. apply max_var_nformulae_mono_aux. apply Pos.le_refl. } rewrite H. apply and_iff_compat_l. apply IHl. eapply agree_env_subset ; eauto. unfold max_var_nformulae. simpl. apply max_var_nformulae_mono_aux'. apply Pos.le_1_l. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat