simp
case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign rhs).getLsb idx✝
no goals