. simp
  rw [BVExpr.bitblast_denote_eq_eval_getLsb]
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size