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