. simp [Ref.hgate]
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
no goals