induction expr generalizing aig with
| const => simp [go]
| literal => simp [go]
| not expr ih => simp [go, ih]
| gate g lhs rhs lih rih => cases g <;> simp [go, Gate.eval, lih, rih]
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
expr : BoolExpr α
aig : AIG α
assign : α → Bool
⊢ ⟦(go expr aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign expr
no goals