apply blastVar.go_decl_eq
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size),
    (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls[idx] = aig.decls[idx]
no goals