cases pred with
| bin lhs op rhs =>
  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)
| getLsb expr idx =>
  simp only [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
aig : AIG BVBit
pred : BVPred
⊢ aig.decls.size ≤ (bitblast aig pred).aig.decls.size
no goals