fact: Definition annot_holds (u: IntMap.ptrie (key:=int) (Annot.t bool)) (s : LitSet.t) := IntMap.fold' (fun (acc:bool) i b => if acc then match b with | None => false | Some b' => match IntMap.get' i u with | Some b2 => Bool.eqb b' (Annot.elt b2) | _ => false end end else acc) s true.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause