apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (mkUlt (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
case bin.ult.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size