trying to split up completeness to save memory
	new file:   Completeness2.agda