simp [ofBoolExprCached.go]
case const
assign : BVExpr.Assignment
a✝ : Bool
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.const a✝) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.const a✝)
no goals