fact: Definition prover_formula thy (up: bool) (m: hmap) (n:nat) (f: HFormula) := if wfb m && chkHc m f.(elt) f.(id) f.(is_dec) then prover_intro (prover_opt thy up n) (insert_unit (annot_lit hTT) (empty_state m)) (Some f) else Fail InternalError.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause