// If n parameter is "computational"

struct ListOfSize{
	int n;

	enum {
		Empty,
		Cons
	} tag;

	union{
		//empty

		//cons
		struct{
			int m;
			bool elt;
			ListOfSize* tail;
		} cons;
	};
};

ListOfSize* tail(int n, ListOfSize* ls){
	return ls->tail;
}

// If n parameter is "non-computational"
// Requires user annotion for n and m

struct ListOfSize{
	//int n; -- erased

	enum {
		Empty,
		Cons
	} tag;

	union{
		//empty

		//cons
		struct{
			//int m; -- erased
			bool elt;
			ListOfSize* tail;
		} cons;
	};
};

ListOfSize* tail(/*int n, -- erased */ ListOfSize* ls){
	return ls->tail;
}