apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
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
case getLsb.h
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (BVExpr.bitblast aig expr).aig.decls.size