rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
α : 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
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
⊢ False
case inl
α : 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
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
v_not_in_c : ¬(v, true) ∈ toList c
⊢ False

case inr
α : 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
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬negateLiteral (v, true) ∈ toList c
⊢ False