fact: Definition only_result_state (st:state) (r: dresult) := match r with | Progress st => only_deps st | Success (hm,d) => is_covered_deps hm d (is_literal_of_state st) | Fail _ => True end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause