data ListOfSize (n:nat)
	empty : ListOfSize 0
	cons : (m:nat) -> (elt:bool) -> ListOfSize m -> ListOfSize (S m)


tail : (n:Nat) -> (ls: ListOfSize (n + 1)) -> ListOfSize n
	case ls of
		cons _ _ ls1 -> ls