rcases h with h | h
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, l.snd) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

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