split at h2
case mp.intro.inr.intro
α : 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
h2 : (if v = l.fst then l.snd else decide ((v, false) ∈ toList c)) = true
⊢ l ∈ toList c
case mp.intro.inr.intro.isTrue
α : 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 : l.snd = true
⊢ l ∈ toList c

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