specialize h (List.ofFn f)
case mp
x : BoolExprNat
h : ∀ (f : List Bool), eval f x = false
f : Fin x.toBoolExpr.vars → Bool
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
case mp
x : BoolExprNat
f : Fin x.toBoolExpr.vars → Bool
h : eval (List.ofFn f) x = false
⊢ BoolExpr.eval f x.toBoolExpr.attach = false