induction expr generalizing aig with
| const => simp [ofBoolExprCached.go]
| literal => simp [ofBoolExprCached.go]
| not expr ih => simp [ofBoolExprCached.go, ih]
| gate g lhs rhs lih rih => cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
expr : BVLogicalExpr
aig : AIG BVBit
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
no goals