fact: Definition wf_units_lit {A:Type} (u: IntMap.ptrie (Annot.t A)) (m: hmap) : Prop := forall i b, IntMap.get' i u = Some b -> valid_index m i /\ wf_pset m (Annot.deps b).
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause