Theorem: BoolExpr.eval_map (LeanSAT/Reflect/BoolExpr/Decidable.lean)

State before:
α β : Type
x : BoolExpr α
f : α → β
g : β → Bool
⊢ eval g (map f x) = eval (g ∘ f) x
Tactic:
cases x <;> simp_all [map, eval, eval_map]
State after:
no goals