unfold lratChecker
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ lratChecker f [] = success → unsatisfiable α f
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ out_of_proof = success → unsatisfiable α f