original.name="Array_Valid_11"
======
>>> main.whiley
function copy(int[] a) -> (int[][] b)
ensures |b| == |a|
ensures all {i in 0..|a| | b[i] == a}:
    int n = |a|
    return [a; n]

public export method test():
    assert copy([]) == []
    assert copy([1]) == [[1]]
    assert copy([1,2]) == [[1,2],[1,2]]
    assert copy([1,2,3]) == [[1,2,3], [1,2,3], [1,2,3]]

---