1 2 3 4 5
concat|T: Type, M: Nat, N: Nat|(l: [T; M], r: [T; N]): [T; M + N] = l + r l = concat [1, 2, 3], [4, 5, 6] _ = l[5] assert l == [1, 2, 3, 4, 5, 6]