. intro h p pl
  apply Exists.intro l.1
  by_cases hl : l.2
  . apply Or.inr
    rw [← hl]
    exact ⟨h, pl⟩
  . apply Or.inl
    simp only [Bool.not_eq_true] at hl
    rw [← hl]
    exact ⟨h, pl⟩
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList c →
    ∀ (p : α → Bool), p ⊨ l → ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
no goals