simp only [HSat.eval, Clause.instHSat, List.any_eq_true, decide_eq_true_eq, Misc.Prod.exists, Misc.Bool.exists_bool,
  empty_eq, List.any_nil] at pf
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
pf : p ⊨ empty
⊢ False
no goals