Function is_mem_contents_all_init Copy item path

pub open spec fn is_mem_contents_all_init<V, const N: usize>(
    arr: [MemContents<V>; N],
) -> bool

{ forall |index: int| 0 <= index < N ==> #[trigger] arr[index].is_init() }