rw [BVExpr.bitblast_denote_eq_eval_getLsb]
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).stream.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
no goals