unfold ofBoolExprCached
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧ = eval assign expr
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr