theorem
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker_sound
{n : Nat}
(f : DefaultFormula n)
(proof : Array IntAction)
(h1 : Formula.ReadyForRupAdd f)
(h2 : Formula.ReadyForRatAdd f)
:
compactLratChecker f proof = Result.success → Unsatisfiable (PosFin n) f