Fixing completeness, part 2.
	modified:   Completeness.agda