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

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

State before:
w : Nat
aig : AIG BVBit
var : BVVar w
⊢ aig.decls.size ≤ (blastVar.go w aig 0 AIG.RefStream.empty var.ident ⋯).aig.decls.size
Tactic:
apply blastVar.go_le_size
State after:
no goals