fact: Definition cnf_plus_and (l : list HFormula) (f:HFormula) (rst: list watched_clause) := match watch_clause_of_list (xrev_map NEG (POS f::nil) l) with | None => rst | Some cl => cl::rst end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause