cases op with
| not => simp [go, ih, hidx]
| shiftLeftConst => simp [go, ih, hidx]
| shiftRightConst =>
  simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
    BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
    decide_eq_true_eq]
  intro h
  apply BitVec.lt_of_getLsb
  assumption
| rotateLeft => simp [go, ih, hidx]
| rotateRight => simp [go, ih, hidx]
| arithShiftRightConst n =>
  rename_i w
  have : ¬(w ≤ idx) := by omega
  simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
case un
w : Nat
assign : Assignment
w✝ : Nat
op : BVUnOp
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✝
⊢ ⟦{ aig := (go aig (un op expr)).val.aig, ref := (go aig (un op expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un op expr)).getLsb idx
no goals