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