simp only [CNF.Clause.eval, List.any_eq_true, bne_iff_ne, ne_eq] at h2
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : eval assign clause = true
⊢ assign ⊨ lratClause
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ assign ⊨ lratClause