Theorem: AIG.ofBoolExprCachedDirect_eval_eq_eval (LeanSAT/AIG/BoolExprCached.lean)

State before:
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
assign : α → Bool
⊢ ⟦ofBoolExprCachedDirect expr, assign⟧ = BoolExpr.eval assign expr
Tactic:
apply ofBoolExprCached.go_eval_eq_eval
State after:
no goals