Fixing completeness.
	modified:   Completeness.agda