give a sufficient precondition for theorem-2
authorHelmut Grohne <helmut@subdivi.de>
Sat, 8 Sep 2012 07:01:57 +0000 (09:01 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Sat, 8 Sep 2012 07:01:57 +0000 (09:01 +0200)
commited83433e106de891931eb3aeb350da5ef8ef0dac
tree3677214f736503f0e1eee2b7bb403d5298744280
parent488f3b4870f63e851f9d3c4ea66bf06222010309
give a sufficient precondition for theorem-2

If get on Fin results in Vecs whose elements are unique, then theorem-2
can be applied.
Precond.agda [new file with mode: 0644]