exact CNF.Clause.mem_lrat_of_mem clause hlit1 h
case intro.intro.left
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : LRAT.DefaultClause.ofArray (List.toArray clause) = some lratClause
lit : PosFin n × Bool
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause
no goals