simp [go, ih, hidx]
case un.rotateRight
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.rotateRight n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.rotateRight n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.rotateRight n✝) expr)).getLsb idx
no goals