proposition: Lemma beval_lit_no_var : forall p b env l, var l <> p -> beval_lit (set_env env p b) l = beval_lit env l.
proof: Proof. unfold beval_lit. intros. unfold set_env. destruct (hformula_eq_dec (var l) p); try congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause