simp only [bitblast]
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ let_fun this := ⋯;
  (bitblast aig (getLsb expr idx)).aig.decls[idx✝] = aig.decls[idx✝]
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls[idx✝] =
    aig.decls[idx✝]