unfold blastVar
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ aig.decls.size ≤ (blastVar aig var).aig.decls.size
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ aig.decls.size ≤ (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size