[| | 0 : nat |]
     : array nat
[| 1; 2; 3 | 0 : nat |]
     : array nat
[| | 0 : nat |]@{Set}
     : array@{Set} nat
[| bool; list nat | nat : Set |]@{prim_array.4}
     : array@{prim_array.4} Set
(* {prim_array.4} |= Set < prim_array.4 *)