rw [← hl]
case pos.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))
case pos.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = true
⊢ (l.fst, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))