Theorem: BVExpr.bitblast.blastVar_decl_eq (LeanSAT/Reflect/BVExpr/BitBlast/Impl/Var.lean)

State before:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (blastVar aig var).aig.decls.size),
    (blastVar aig var).aig.decls[idx] = aig.decls[idx]
Tactic:
unfold blastVar
State after:
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]

State before:
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]
Tactic:
apply blastVar.go_decl_eq
State after:
no goals