apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
case getLsb.h2
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < (BVExpr.bitblast aig expr).aig.decls.size
case getLsb.h2.h
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < aig.decls.size