def read_list_of (n:nat) : ListOfSize n
	case n of
		0 -> empty
		S m ->
			elt <- read_bool
			tail <- read_list_of m
			cons m v tail

def read_list : (n:nat, ListOfSize n)
	n <- read_nat
	ls <- read_list_of n
	(n, ls)