next action restPrf ih =>
simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
unfold lratChecker
split
. intro h
  exfalso
  simp only at h
. next id rupHints restPrf' _ =>
  simp only [ite_eq_left_iff, Bool.not_eq_true]
  intro rupAddSuccess
  rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
  exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
. next id c rupHints restPrf' hprf =>
  split
  next f' checkSuccess heq =>
  split
  . next hCheckSuccess =>
    intro f'_success
    simp only [List.cons.injEq] at hprf
    rw [← hprf.2] at f'_success
    rw [hCheckSuccess] at heq
    exact addRupCaseSound f f_readyForRupAdd f_readyForRatAdd c f' rupHints heq restPrf restPrfWellFormed ih f'_success
  . simp only [false_implies]
. next id c pivot rupHints ratHints restPrf' hprf =>
  split
  next f' checkSuccess heq =>
  split
  . next hCheckSuccess =>
    intro f'_success
    simp only [List.cons.injEq] at hprf
    rw [← hprf.2] at f'_success
    rw [hCheckSuccess] at heq
    simp only [wellFormedAction, hprf.1] at actionWellFormed
    exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
      restPrfWellFormed ih f'_success
  . simp only [false_implies]
. next ids restPrf' hprf =>
  intro h
  simp only [List.cons.injEq] at hprf
  rw [← hprf.2] at h
  exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
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
no goals