apply BitVec.lt_of_getLsb
case un.shiftRightConst
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
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ n✝ + idx < w✝
case un.shiftRightConst.a
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
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ ?un.shiftRightConst.x.getLsb (n✝ + idx) = true

case un.shiftRightConst.x
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
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ BitVec w✝