Theorem: BVExpr.bitblast_le_size (LeanSAT/Reflect/BVExpr/BitBlast/Impl/Expr.lean)

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

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ aig.decls.size ≤ (bitblast.go aig expr).val.aig.decls.size
Tactic:
exact (bitblast.go aig expr).property
State after:
no goals