. apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  assumption
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
no goals