cases op with
| eq =>
  simp [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
| ult =>
  simp [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
case bin
aig : AIG BVBit
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs op rhs)).aig.decls.size
no goals