simp only [bitblast]
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (bitblast aig (getLsb expr idx)).aig.decls.size
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤
    (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls.size