Almost everything typechecks in Completeness.agda
	modified:   Completeness.agda