simp [bitblast]
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs BVBinPred.eq rhs)).aig.decls.size
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls.size