[Agda] another possible without-K problem

[Altenkirch Thorsten]

DQoNCk9uIDEwLzA3LzIwMTMgMTU6NTIsICJEYW4gTGljYXRhIiA8ZHJsQGNzLmNtdS5lZHU+IHdy
b3RlOg0KDQo+SXMgdGhpcyBhIGJ1ZyBvciBhIGRlc2lnbiBkZWNpc2lvbj8gIEl0IHNlZW1zIGxp
a2UgdGhpcyBleGFtcGxlIGlzIGluDQo+YWNjb3JkIHdpdGggdGhlIGRlc2NyaXB0aW9uIG9mIHdp
dGhvdXQtSyBpbiB0aGUgcmVsZWFzZSBub3RlcywgYnV0DQo+dGhhdCBhbGxvd2luZyBtYXRjaGlu
ZyB3aGVuIHRoZSBpbmRpY2VzIGFyZSBjb25zdHJ1Y3RvcnMgaGFzIHNvbWUNCj5pbnRlcmVzdGlu
ZyBjb25zZXF1ZW5jZXMuDQoNCllvdSBhcmUgcmlnaHQgc2luY2UgaW4gdGhlIGV4YW1wbGUgUzEg
aXMganVzdCBhbiBpbmR1Y3RpdmUgdHlwZSB0aGlzIGlzbid0DQpyZWFsbHkgYSBwcm9ibGVtLiAN
Cg0KSXMgdGhpcyBzdGlsbCBwb3NzaWJsZSBpZiBvbmUgImhpZGVzIiB0aGUgZmFjdCB0aGF0IFMx
IGlzIGluZHVjdGl2ZWx5DQpkZWZpbmVkPw0KSSBndWVzcyB0aGlzIGlzIG1vcmUgdGhlIHByb2Js
ZW0gdGhhdCB0aGUgY3VycmVudCBpbXBsZW1lbnRhdGlvbiBvZiBISVRzDQppcyBhIGJpdCBvZiBh
IGhhY2suDQoNCkRpc2pvaW50bmVzcyB3YXMgYWx3YXlzIGJ1aWx0IGludG8gcGF0dGVybiBtYXRj
aGluZyBhbmQgaXQgaXMgaGFyZCB0byBzZWUNCmhvdyB0byBhdm9pZCB0aGlzLg0KT25lIG9ubHkg
bmVlZHMgYSBtaWNyb3Njb3BpYyB1bml2ZXJzZSwgQm9vbCB3aXRoIFQgOiBCb29sIC0+IFR5cGUg
dG8NCmp1c3RpZnkgdGhpcy4NCg0KVGhvcnN0ZW4NCg0KPiBJbiBwYXJ0aWN1bGFyLCBpdCBtZWFu
cyB0aGF0LCBpbiBhIGNvcmUNCj50aGVvcnkgd2l0aG91dCB1bml2ZXJzZXMsIHdpdGhvdXQtSyBw
YXR0ZXJuIG1hdGNoaW5nIGNhbm5vdCBiZQ0KPmNvbXBpbGVkIHRvIEosIGJlY2F1c2UgeW91IGNh
biBwcm92ZSBkaXNqb2ludG5lc3MgKGFuZCBpbmplY3Rpdml0eSkgb2YNCj5jb25zdHJ1Y3RvcnMs
IGFuZCB0aGF0IGJvb2wgaXMgYW4gaHNldCAoY29kZSBiZWxvdyksIGp1c3QgdXNpbmcNCj5wYXR0
ZXJuIG1hdGNoaW5nIG9uIHRoZSBpZGVudGl0eSB0eXBlLiAgQXMgZmFyIGFzIEkga25vdywgZGlz
am9pbnRuZXNzDQo+YW5kIHRoZSBoc2V0LW5lc3Mgb2YgYm9vbCByZXF1aXJlIGEgdW5pdmVyc2Uv
bGFyZ2UgZWxpbXMgdG8gcHJvdmUuICBPZg0KPmNvdXJzZSwgQWdkYSBoYXMgdW5pdmVyc2VzLCBh
bmQgaXQgaXMgcG9zc2libGUgdGhhdCB3aXRob3V0LUsgcGF0dGVybg0KPm1hdGNoaW5nIGNvdWxk
IGJlIGNvbXBpbGVkIHRvIEogKyB1c2VzIG9mIGxhcmdlIGVsaW1zIHRvIGNvZGUgdXAgdGhlc2UN
Cj5jb25zdHJ1Y3Rpb25zIG9uIGNvbnN0cnVjdG9ycy4gIEJ1dCBJIHdvdWxkIHBlcnNvbmFsbHkg
cHJlZmVyIGl0IGlmDQo+d2l0aG91dC1LIHBhdHRlcm4gbWF0Y2hpbmcgZGlkIG5vdCBidWlsZCB0
aGVzZSB0aGluZ3MgaW4sIGJlY2F1c2UgaXQNCj5tZWFucyB3ZSBuZWVkIHRvIHVzZSB0d28gaGFj
a3MgKHJhdGhlciB0aGFuIGp1c3Qgb25lIDopICkgdG8gaW1wbGVtZW50DQo+aGlnaGVyIGluZHVj
dGl2ZXMuDQo+DQo+LURhbg0KPg0KPi0tIGNoZWNrcyBpbiBBZ2RhIDIuMy4yLjENCj57LSMgT1BU
SU9OUyAtLXdpdGhvdXQtSyAjLX0NCj4NCj5tb2R1bGUgV2l0aG91dEsgd2hlcmUNCj4NCj4gIGRh
dGEgTmF0IDogU2V0IHdoZXJlDQo+ICAgIFogOiBOYXQNCj4gICAgUyA6IE5hdCAtPiBOYXQNCj4N
Cj4gIGRhdGEgQm9vbCA6IFNldCB3aGVyZQ0KPiAgICBUcnVlIDogQm9vbA0KPiAgICBGYWxzZSA6
IEJvb2wNCj4NCj4gIGRhdGEgVm9pZCA6IFNldCB3aGVyZQ0KPg0KPiAgZGF0YSBfPT1fIHtBIDog
U2V0fSAoeCA6IEEpIDogQSAtPiBTZXQgd2hlcmUNCj4gICAgUmVmbCA6IHggPT0geA0KPg0KPiAg
aW5qZWN0aXZlIDoge20gbiA6IE5hdH0gLT4gUyBtID09IFMgbiAtPiBtID09IG4NCj4gIGluamVj
dGl2ZSBSZWZsID0gUmVmbA0KPg0KPiAgZGlzam9pbnQgOiB7bSA6IE5hdH0gLT4gUyBtID09IFog
LT4gVm9pZA0KPiAgZGlzam9pbnQgKCkNCj4NCj4gIGJvb2wtaHNldCA6IChiIDogQm9vbCkgLT4g
KHAgOiBiID09IGIpIC0+IHAgPT0gUmVmbA0KPiAgYm9vbC1oc2V0IFRydWUgUmVmbCA9IFJlZmwN
Cj4gIGJvb2wtaHNldCBGYWxzZSBSZWZsID0gUmVmbA0KPg0KPg0KPg0KPk9uIFdlZCwgSnVsIDEw
LCAyMDEzIGF0IDU6NTYgQU0sIEFsdGVua2lyY2ggVGhvcnN0ZW4NCj48cHN6dHhhQGV4bWFpbC5u
b3R0aW5naGFtLmFjLnVrPiB3cm90ZToNCj4+IFRoaXMgbG9va3MgbGlrZSBhIGJ1ZyChViBwbGVh
c2UgYWRkIGl0IHRvIHRoZSBidWcgdHJhY2tlci4NCj4+DQo+PiBXZSByZWFsbHkgbmVlZCB0byB1
bmRlcnN0YW5kIHdoYXQgd2UgYXJlIGRvaW5nIHdoZW4gY2hlY2tpbmcgd2V0aGVyDQo+PnBhdHRl
cm4NCj4+IHNhdGlzZnkgdGhlIKFYd2l0aG91dC1LIGNvbmRpdGlvbi4gSXQgc2VlbXMgdGhhdCBD
b25vcidzIHdvcmsgb24NCj4+dHJhbnNsYXRpbmcNCj4+IHBhdHRlcm4gbWF0Y2hpbmcgdG8gZWxp
bWluYXRvcnMgKHdpdGggSiBhbmQgSykgd291bGQgYmUgYSBnb29kIHN0YXJ0aW5nDQo+PiBwb2lu
dC4NCj4+DQo+PiBBdCB0aGUgc2FtZSB0aW1lIHdlIGtub3cgdGhhdCBtYW55IHR5cGVzIHN1cHBv
cnQgVUlQIGJ5IHN0cnVjdHVyZS4NCj4+TWljaGFlbA0KPj4gSGVkYmVyZyBzaG93ZWQgdGhhdCBh
bGwgdHlwZXMgd2l0aCBhIGRlY2lkYWJsZSBlcXVhbGl0eSBzdXBwb3J0IFVJUCBhbmQNCj4+aXQN
Cj4+IGlzIG5vdCBoYXJkIHRvIHNlZSB0aGF0IHRoaXMgY2FuIGJlIGV4dGVuZGVkIHRvIHN0YWJs
ZSBlcXVhbGl0eSAobm9uLW5vdA0KPj4gY2xvc2VkKS4gKExpdHRsZSBwdXp6bGU6IHdpdGhvdXQg
ZXh0ZW5zaW9uYWxpdHkgoVYgYXJlIHRoZXJlIGFueSB0eXBlcw0KPj53aGljaA0KPj4gaGF2ZSBz
dGFibGUgYnV0IG5vdCBkZWNpZGFibGUgZXF1YWxpdHkgPykNCj4+DQo+PiBXZSBhbHNvIHdhbnQg
dG8gcXVhbnRpZnkgb3ZlciBhbGwgSFNldHMgKEkuZS4gdHlwZXMgd2l0aCBVSVApIGFuZCBzbyBv
bi4NCj4+DQo+PiBUaG9yc3Rlbg0KPj4NCj4+IEZyb206IEphc29uIFJlZWQgPGpjcmVlZEBnbWFp
bC5jb20+DQo+PiBEYXRlOiBUdWUsIDkgSnVsIDIwMTMgMTY6MzE6MjIgKzAxMDANCj4+IFRvOiAi
YWdkYUBsaXN0cy5jaGFsbWVycy5zZSIgPGFnZGFAbGlzdHMuY2hhbG1lcnMuc2U+DQo+PiBTdWJq
ZWN0OiBbQWdkYV0gYW5vdGhlciBwb3NzaWJsZSB3aXRob3V0LUsgcHJvYmxlbQ0KPj4NCj4+IEkn
bSBleHBlcmllbmNpbmcgc29tZXRoaW5nIHRoYXQgSSB0aGluayBpcyBhIHZpb2xhdGlvbiBvZiB0
aGUgaW50ZW50IG9mDQo+PnRoZQ0KPj4gLS13aXRob3V0LUsgZmxhZywgc2ltaWxhciB0byB3aGF0
IFRob3JzdGVuIHdhcyB0YWxraW5nIGFib3V0IGluDQo+PiBodHRwczovL2xpc3RzLmNoYWxtZXJz
LnNlL3BpcGVybWFpbC9hZ2RhLzIwMTIvMDA0MTA0Lmh0bWwuDQo+Pg0KPj4gVGhlIGZvbGxvd2lu
ZyBmaWxlIGNoZWNrcyBmaW5lIGZvciBtZSB1bmRlciBjdXJyZW50IGRhcmNzIEFnZGE6DQo+Pg0K
Pj4gPDw8YmVnaW4+Pj4NCj4+IHstIyBPUFRJT05TIC0td2l0aG91dC1LICMtfQ0KPj4NCj4+IG1v
ZHVsZSBUZXN0IHdoZXJlDQo+Pg0KPj4gZGF0YSBTMSA6IFNldCB3aGVyZQ0KPj4gICAgIGJhc2Ug
OiBTMQ0KPj4NCj4+IG1vZHVsZSB0ZXN0IHdoZXJlDQo+PiAgICBkYXRhIF+h3V8ge0EgOiBTZXR9
IChhIDogQSkgOiBBIKH3IFNldCB3aGVyZQ0KPj4gICAgIHJlZmwgOiBhIKHdIGENCj4+DQo+PiAg
ICBiYWQgOiAocCBxIDogYmFzZSCh3SBiYXNlKSAtPiBwIKHdIHENCj4+ICAgIGJhZCByZWZsIHJl
ZmwgPSByZWZsDQo+Pg0KPj4gbW9kdWxlIHRlc3QyIHdoZXJlDQo+PiAgICBkYXRhIF+h3V8ge0Eg
OiBTZXR9IDogQSCh9yBBIKH3IFNldCB3aGVyZQ0KPj4gICAgICAgIHJlZmwgOiB7eCA6IEF9IKH3
IHggod0geA0KPj4NCj4+ICAgIGJhZCA6IChwIHEgOiBiYXNlIKHdIGJhc2UpIC0+IHAgod0gcQ0K
Pj4gICAgYmFkIHJlZmwgcmVmbCA9IHJlZmwNCj4+IDw8PGVuZD4+Pg0KPj4NCj4+IE5vdGUgdGhh
dCB0aGlzIGNvdmVycyBib3RoIHRoZSBwb3NzaWJsZSBkZWZpbml0aW9ucyBvZiB0aGUgaWRlbnRp
dHkgdHlwZQ0KPj4gbWVudGlvbmVkIGJ5IEd1aWxsYXVtZSBpbg0KPj4gaHR0cHM6Ly9saXN0cy5j
aGFsbWVycy5zZS9waXBlcm1haWwvYWdkYS8yMDEyLzAwNDEwNS5odG1sDQo+Pg0KPj4gQW55IGlk
ZWFzIHdoYXQgc2hvdWxkIGJlIGRvbmUgaGVyZT8gRG9lcyB0aGUgSy1jaGVjayBuZWVkIHRvIGJl
IGZ1cnRoZXINCj4+IHN0cmVuZ3RoZW5lZCB3aGVuIHRoZXJlIGFyZW4ndCBwYXJhbWV0ZXJzIGFy
b3VuZD8gQW0gSSBtaXN1bmRlcnN0YW5kaW5nDQo+PiBzb21ldGhpbmcgdHJpdmlhbD8NCj4+DQo+
Pg0KPj4gVGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNobWVudCBhcmUgaW50ZW5kZWQgc29sZWx5
IGZvciB0aGUgYWRkcmVzc2VlDQo+PmFuZA0KPj4gbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGlu
Zm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzIG1lc3NhZ2UNCj4+aW4NCj4+IGVy
cm9yLCBwbGVhc2Ugc2VuZCBpdCBiYWNrIHRvIG1lLCBhbmQgaW1tZWRpYXRlbHkgZGVsZXRlIGl0
LiAgIFBsZWFzZQ0KPj5kbyBub3QNCj4+IHVzZSwgY29weSBvciBkaXNjbG9zZSB0aGUgaW5mb3Jt
YXRpb24gY29udGFpbmVkIGluIHRoaXMgbWVzc2FnZSBvciBpbg0KPj5hbnkNCj4+IGF0dGFjaG1l
bnQuICBBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5IHRoZSBhdXRob3Igb2YgdGhp
cw0KPj5lbWFpbCBkbw0KPj4gbm90IG5lY2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9mIHRo
ZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0uDQo+Pg0KPj4gVGhpcyBtZXNzYWdlIGhhcyBiZWVu
IGNoZWNrZWQgZm9yIHZpcnVzZXMgYnV0IHRoZSBjb250ZW50cyBvZiBhbg0KPj5hdHRhY2htZW50
DQo+PiBtYXkgc3RpbGwgY29udGFpbiBzb2Z0d2FyZSB2aXJ1c2VzIHdoaWNoIGNvdWxkIGRhbWFn
ZSB5b3VyIGNvbXB1dGVyDQo+PnN5c3RlbSwNCj4+IHlvdSBhcmUgYWR2aXNlZCB0byBwZXJmb3Jt
IHlvdXIgb3duIGNoZWNrcy4gRW1haWwgY29tbXVuaWNhdGlvbnMgd2l0aA0KPj50aGUNCj4+IFVu
aXZlcnNpdHkgb2YgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRvcmVkIGFzIHBlcm1pdHRlZCBieSBV
Sw0KPj5sZWdpc2xhdGlvbi4NCj4+DQo+Pg0KPj4NCj4+IF9fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fDQo+PiBBZ2RhIG1haWxpbmcgbGlzdA0KPj4gQWdkYUBs
aXN0cy5jaGFsbWVycy5zZQ0KPj4gaHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xp
c3RpbmZvL2FnZGENCj4+DQoNCg==