[Agda] another possible without-K problem

[Altenkirch Thorsten]

DQoNCk9uIDEwLzA3LzIwMTMgMTM6MDAsICJBbmRyZWFzIEFiZWwiIDxhbmRyZWFzLmFiZWxAaWZp
LmxtdS5kZT4gd3JvdGU6DQoNCj5PbiAxMC4wNy4yMDEzIDExOjU2LCBBbHRlbmtpcmNoIFRob3Jz
dGVuIHdyb3RlOg0KPj4gVGhpcyBsb29rcyBsaWtlIGEgYnVnIKFWIHBsZWFzZSBhZGQgaXQgdG8g
dGhlIGJ1ZyB0cmFja2VyLg0KPg0KPkkgYWRkZWQgdGhpcyBhcyBpc3N1ZSA4ODEuDQo+DQo+PiBX
ZSByZWFsbHkgbmVlZCB0byB1bmRlcnN0YW5kIHdoYXQgd2UgYXJlIGRvaW5nIHdoZW4gY2hlY2tp
bmcgd2V0aGVyDQo+PiBwYXR0ZXJuIHNhdGlzZnkgdGhlIKFYd2l0aG91dC1LIGNvbmRpdGlvbi4g
SXQgc2VlbXMgdGhhdCBDb25vcidzIHdvcmsgb24NCj4+IHRyYW5zbGF0aW5nIHBhdHRlcm4gbWF0
Y2hpbmcgdG8gZWxpbWluYXRvcnMgKHdpdGggSiBhbmQgSykgd291bGQgYmUgYQ0KPj4gZ29vZCBz
dGFydGluZyBwb2ludC4NCj4NCj5Db3VsZCBub3QgYWdyZWUgbW9yZSENCj4NCj4+IEF0IHRoZSBz
YW1lIHRpbWUgd2Uga25vdyB0aGF0IG1hbnkgdHlwZXMgc3VwcG9ydCBVSVAgYnkgc3RydWN0dXJl
Lg0KPj4gTWljaGFlbCBIZWRiZXJnIHNob3dlZCB0aGF0IGFsbCB0eXBlcyB3aXRoIGEgZGVjaWRh
YmxlIGVxdWFsaXR5IHN1cHBvcnQNCj4+IFVJUCBhbmQgaXQgaXMgbm90IGhhcmQgdG8gc2VlIHRo
YXQgdGhpcyBjYW4gYmUgZXh0ZW5kZWQgdG8gc3RhYmxlDQo+PiBlcXVhbGl0eSAobm9uLW5vdCBj
bG9zZWQpLiAoTGl0dGxlIHB1enpsZTogd2l0aG91dCBleHRlbnNpb25hbGl0eSChViBhcmUNCj4+
IHRoZXJlIGFueSB0eXBlcyB3aGljaCBoYXZlIHN0YWJsZSBidXQgbm90IGRlY2lkYWJsZSBlcXVh
bGl0eSA/KQ0KPg0KPldoYXQgd2FzICJub24tbm90IGNsb3NlZCIgYWdhaW4/DQoNCm5vdCAobm90
IEEpIC0+IEENCj0gc3RhYmxlDQoNCkFjY29yZGluZyB0byBNYXJ0aW4gRXNjYXJkbyBhIHR5cGUg
d2l0aCBzdGFibGUgZXF1YWxpdHkgY2FuIGJlIGNhbGxlZA0Kc2VwYXJhdGVkLCB3aGlsZSBhIHR5
cGUgd2l0aA0KDQpULg0KDQo+DQo+PiBXZSBhbHNvIHdhbnQgdG8gcXVhbnRpZnkgb3ZlciBhbGwg
SFNldHMgKEkuZS4gdHlwZXMgd2l0aCBVSVApIGFuZCBzbyBvbi4NCj4NCj4+IEZyb206IEphc29u
IFJlZWQgPGpjcmVlZEBnbWFpbC5jb20gPG1haWx0bzpqY3JlZWRAZ21haWwuY29tPj4NCj4+IERh
dGU6IFR1ZSwgOSBKdWwgMjAxMyAxNjozMToyMiArMDEwMA0KPj4gVG86ICJhZ2RhQGxpc3RzLmNo
YWxtZXJzLnNlIDxtYWlsdG86YWdkYUBsaXN0cy5jaGFsbWVycy5zZT4iDQo+PiA8YWdkYUBsaXN0
cy5jaGFsbWVycy5zZSA8bWFpbHRvOmFnZGFAbGlzdHMuY2hhbG1lcnMuc2U+Pg0KPj4gU3ViamVj
dDogW0FnZGFdIGFub3RoZXIgcG9zc2libGUgd2l0aG91dC1LIHByb2JsZW0NCj4+DQo+PiAgICAg
SSdtIGV4cGVyaWVuY2luZyBzb21ldGhpbmcgdGhhdCBJIHRoaW5rIGlzIGEgdmlvbGF0aW9uIG9m
IHRoZSBpbnRlbnQNCj4+ICAgICBvZiB0aGUgLS13aXRob3V0LUsgZmxhZywgc2ltaWxhciB0byB3
aGF0IFRob3JzdGVuIHdhcyB0YWxraW5nIGFib3V0DQo+PiAgICAgaW4gaHR0cHM6Ly9saXN0cy5j
aGFsbWVycy5zZS9waXBlcm1haWwvYWdkYS8yMDEyLzAwNDEwNC5odG1sLg0KPj4NCj4+ICAgICBU
aGUgZm9sbG93aW5nIGZpbGUgY2hlY2tzIGZpbmUgZm9yIG1lIHVuZGVyIGN1cnJlbnQgZGFyY3Mg
QWdkYToNCj4+DQo+PiAgICAgPDw8YmVnaW4+Pj4NCj4+ICAgICB7LSMgT1BUSU9OUyAtLXdpdGhv
dXQtSyAjLX0NCj4+DQo+PiAgICAgbW9kdWxlIFRlc3Qgd2hlcmUNCj4+DQo+PiAgICAgZGF0YSBT
MSA6IFNldCB3aGVyZQ0KPj4gICAgICAgICAgYmFzZSA6IFMxDQo+Pg0KPj4gICAgIG1vZHVsZSB0
ZXN0IHdoZXJlDQo+PiAgICAgICAgIGRhdGEgX6HdXyB7QSA6IFNldH0gKGEgOiBBKSA6IEEgofcg
U2V0IHdoZXJlDQo+PiAgICAgICAgICByZWZsIDogYSCh3SBhDQo+Pg0KPj4gICAgICAgICBiYWQg
OiAocCBxIDogYmFzZSCh3SBiYXNlKSAtPiBwIKHdIHENCj4+ICAgICAgICAgYmFkIHJlZmwgcmVm
bCA9IHJlZmwNCj4+DQo+PiAgICAgbW9kdWxlIHRlc3QyIHdoZXJlDQo+PiAgICAgICAgIGRhdGEg
X6HdXyB7QSA6IFNldH0gOiBBIKH3IEEgofcgU2V0IHdoZXJlDQo+PiAgICAgICAgICAgICByZWZs
IDoge3ggOiBBfSCh9yB4IKHdIHgNCj4+DQo+PiAgICAgICAgIGJhZCA6IChwIHEgOiBiYXNlIKHd
IGJhc2UpIC0+IHAgod0gcQ0KPj4gICAgICAgICBiYWQgcmVmbCByZWZsID0gcmVmbA0KPj4gICAg
IDw8PGVuZD4+Pg0KPj4NCj4+ICAgICBOb3RlIHRoYXQgdGhpcyBjb3ZlcnMgYm90aCB0aGUgcG9z
c2libGUgZGVmaW5pdGlvbnMgb2YgdGhlIGlkZW50aXR5DQo+PiAgICAgdHlwZSBtZW50aW9uZWQg
YnkgR3VpbGxhdW1lIGluDQo+PiAgICAgaHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9waXBlcm1h
aWwvYWdkYS8yMDEyLzAwNDEwNS5odG1sDQo+Pg0KPj4gICAgIEFueSBpZGVhcyB3aGF0IHNob3Vs
ZCBiZSBkb25lIGhlcmU/IERvZXMgdGhlIEstY2hlY2sgbmVlZCB0byBiZQ0KPj4gICAgIGZ1cnRo
ZXIgc3RyZW5ndGhlbmVkIHdoZW4gdGhlcmUgYXJlbid0IHBhcmFtZXRlcnMgYXJvdW5kPyBBbSBJ
DQo+PiAgICAgbWlzdW5kZXJzdGFuZGluZyBzb21ldGhpbmcgdHJpdmlhbD8NCj4+DQo+Pg0KPj4g
VGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNobWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0
aGUgYWRkcmVzc2VlDQo+PiBhbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0aW9u
LiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzDQo+PiBtZXNzYWdlIGluIGVycm9yLCBwbGVhc2Ug
c2VuZCBpdCBiYWNrIHRvIG1lLCBhbmQgaW1tZWRpYXRlbHkgZGVsZXRlDQo+PiBpdC4gICBQbGVh
c2UgZG8gbm90IHVzZSwgY29weSBvciBkaXNjbG9zZSB0aGUgaW5mb3JtYXRpb24gY29udGFpbmVk
IGluDQo+PiB0aGlzIG1lc3NhZ2Ugb3IgaW4gYW55IGF0dGFjaG1lbnQuICBBbnkgdmlld3Mgb3Ig
b3BpbmlvbnMgZXhwcmVzc2VkIGJ5DQo+PiB0aGUgYXV0aG9yIG9mIHRoaXMgZW1haWwgZG8gbm90
IG5lY2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9mIHRoZQ0KPj4gVW5pdmVyc2l0eSBvZiBO
b3R0aW5naGFtLg0KPj4NCj4+IFRoaXMgbWVzc2FnZSBoYXMgYmVlbiBjaGVja2VkIGZvciB2aXJ1
c2VzIGJ1dCB0aGUgY29udGVudHMgb2YgYW4NCj4+IGF0dGFjaG1lbnQgbWF5IHN0aWxsIGNvbnRh
aW4gc29mdHdhcmUgdmlydXNlcyB3aGljaCBjb3VsZCBkYW1hZ2UgeW91cg0KPj4gY29tcHV0ZXIg
c3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQgdG8gcGVyZm9ybSB5b3VyIG93biBjaGVja3MuIEVtYWls
DQo+PiBjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5
IGJlIG1vbml0b3JlZCBhcw0KPj4gcGVybWl0dGVkIGJ5IFVLIGxlZ2lzbGF0aW9uLg0KPj4NCj4+
DQo+Pg0KPj4NCj4+IF9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fDQo+PiBBZ2RhIG1haWxpbmcgbGlzdA0KPj4gQWdkYUBsaXN0cy5jaGFsbWVycy5zZQ0KPj4g
aHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGENCj4+DQo+DQo+
DQo+LS0gDQo+QW5kcmVhcyBBYmVsICA8PjwgICAgICBEdSBiaXN0IGRlciBnZWxpZWJ0ZSBNZW5z
Y2guDQo+DQo+VGhlb3JldGljYWwgQ29tcHV0ZXIgU2NpZW5jZSwgVW5pdmVyc2l0eSBvZiBNdW5p
Y2gNCj5PZXR0aW5nZW5zdHIuIDY3LCBELTgwNTM4IE11bmljaCwgR0VSTUFOWQ0KPg0KPmFuZHJl
YXMuYWJlbEBpZmkubG11LmRlDQo+aHR0cDovL3d3dzIudGNzLmlmaS5sbXUuZGUvfmFiZWwvDQoN
Cg==