. unfold lratChecker
  simp only [false_implies]
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 cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f