rw [← hl] at h
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 = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, l.snd) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause