unfold bitblast
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦expr.bitblast, assign.toAIGAssignment⟧
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧