unfold bitblast
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ aig.decls.size ≤ (bitblast aig expr).aig.decls.size
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ aig.decls.size ≤ (bitblast.go aig expr).val.aig.decls.size