fact: Fixpoint beval_clause (env : HFormula -> bool) (cl : clause) := match cl with | nil => false | e::cl' => beval_lit env e || beval_clause env cl' end.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List Cdcl.Lib Cdcl.Syntax Cdcl.Lit