proposition: Lemma beval_no_var : forall p l b env, ~ is_var_of_cnf p l -> beval_cnf (set_env env p b) l = beval_cnf env l.
proof: Proof. intros. induction l. - simpl. reflexivity. - simpl. rewrite is_var_of_cnf_cons in H. rewrite IHl by tauto. f_equal. apply beval_clause_no_var. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause