a bit more proof equationalizing, and now I've broken my Agda by trying to rebuild it on OS X mavericks...
	modified:   Fin.agda
	modified:   WellScopedTerms.agda