specialize h p pl
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
⊢ l ∈ toList c
case mp
α : 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
h : ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c