fact: Definition mklform (f : HFormula) : HFormula := if is_TT f.(elt) then hTT else f.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause