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