proposition: Lemma eval_clause_of_opt : forall env l, beval_cnf env (clause_of_opt l) = negb (boeval env l).
proof: Proof. destruct l;simpl. unfold beval_lit. simpl. btauto. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause