Theorem: BVExpr.bitblast.go_val_eq_bitblast (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Expr.lean)

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ (go aig expr).val = bitblast aig expr
Tactic:
rfl
State after:
no goals