intro incrementalChecker_success p pf
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = success → unsatisfiable α f
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success : (incrementalLRATChecker f a).snd = success
p : α → Bool
pf : p ⊨ f
⊢ False