data List a where
    Nil :: List a
    Cons :: x: a -> xs: List a -> List a

data Pair a b where
    Pair :: a -> b -> Pair a b

termination measure len :: List a -> {Int | _v >= 0} where
    Nil -> 0
    Cons x xs -> 1 + len xs

zip :: l1:(List a) -> {List b | len _v == len l1} -> {List (Pair a b) | len _v == len l1}
zip = ??

unzip :: l:(List (Pair a b)) -> (Pair {List a | len _v == len l} {List b | len _v == len l})
unzip = ?? -- できない

-- ここまで書いてあげるとできるが、ほぼ答え
unzip :: l:(List (Pair a b)) -> (Pair {List a | len _v == len l} {List b | len _v == len l})
unzip = \l.
    match l with
        Nil -> Pair Nil Nil
        Cons x xs -> match unzip xs with
                         Pair as bs -> match x with
                                           Pair a b -> ??