fact: Definition progress_arrow (l:literal) (st:state): bool := match find_lit (POS (form_of_literal l)) (units st) with | None => true | Some b => Annot.lift negb b end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause