Theorem: BVExpr.Assignment.toAIGAssignment_apply (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Basic.lean)

State before:
assign : Assignment
bit : BVBit
⊢ assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsb ↑bit.idx
Tactic:
rfl
State after:
no goals