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