simp only [unsat, BoolExpr.unsat]
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.attach.unsat
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) ↔
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false