drop the injection requirement for gl₁
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 14 Oct 2014 07:52:00 +0000 (09:52 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 14 Oct 2014 07:52:00 +0000 (09:52 +0200)
commitb1b80567288030782231418407e7244b37227450
tree59f8235071780a89505166349b7bc2f7af03d9e5
parentf9fc1aba9386216a6a01ba17d85fcae71756d928
drop the injection requirement for gl₁

Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.
Examples.agda
FreeTheorems.agda
GetTypes.agda