removed unneeded experimental irrelevance flag
	modified:   Completeness.agda