dsimp [eval]
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ eval f x.not = eval g x.not
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ (!eval f x) = !eval g x