rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.bitblast aig expr).aig.decls[idx✝] = aig.decls[idx✝]

case getLsb.h1
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
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