. next v_ne_l =>
  simp only [decide_eq_true_eq] at h2
  exfalso
  rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
  . exact v_not_in_c h1
  . simp only [negateLiteral, Bool.not_true] at negv_not_in_c
    exact negv_not_in_c h2
case mp.intro.inr.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c
no goals