. simp only [hl, Bool.not_true]
  rw [← hl] at h
  rcases h with h | h
  . exact Or.inl h
  . exact Or.inr h
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause