have : ¬(w ≤ idx) := by omega
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
this : ¬w ≤ idx
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx