simp only [HSat.eval, List.any_eq_true, decide_eq_true_eq]
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
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
⊢ ∃ x, x ∈ LRAT.Clause.toList lratClause ∧ assign x.fst = x.snd