open import Pervasives type bit = O | I | U type vector 'a = V of list 'a * nat * bool let rec nth xs (n : nat) = match (n,xs) with | (0,x :: xs) -> x | (n + 1,x :: xs) -> nth xs n end