proposition: Lemma beval_clause_no_var : forall p b env cl, ~ is_var_of_clause p cl -> beval_clause (set_env env p b) cl = beval_clause env cl.
proof: Proof. induction cl;simpl. - reflexivity. - rewrite is_var_of_clause_cons. intros. rewrite IHcl by tauto. rewrite beval_lit_no_var by tauto. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause