∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w : ℕ) (aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (lhs : aig_1.RefVec w),
  aig.decls.size ≤ { aig := aig_1, vec := lhs }.aig.decls.size →
    ∀ (aig_2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (rhs : aig_2.RefVec w)
      (hraig : aig_1.decls.size ≤ { aig := aig_2, vec := rhs }.aig.decls.size),
      aig.decls.size ≤
        (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul aig_2 { lhs := lhs.cast hraig, rhs := rhs }).aig.decls.size