dsimp [go]
case const
w idx w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (const val✝)).val.aig.decls.size
⊢ (go aig (const val✝)).val.aig.decls[idx] = aig.decls[idx]
case const
w idx w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (const val✝)).val.aig.decls.size
⊢ (blastConst aig val✝).aig.decls[idx] = aig.decls[idx]