intro h2
n : Nat
lratClause : LRAT.DefaultClause n
assign : PosFin n → Bool
clause : Clause (PosFin n)
h : clause.convertLRAT' = some lratClause
⊢ 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 : eval assign clause = true
⊢ assign ⊨ lratClause