diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-08 09:01:57 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-08 09:01:57 +0200 |
| commit | ed83433e106de891931eb3aeb350da5ef8ef0dac (patch) | |
| tree | 3677214f736503f0e1eee2b7bb403d5298744280 /CheckInsert.agda | |
| parent | 488f3b4870f63e851f9d3c4ea66bf06222010309 (diff) | |
| download | bidiragda-ed83433e106de891931eb3aeb350da5ef8ef0dac.tar.gz | |
give a sufficient precondition for theorem-2
If get on Fin results in Vecs whose elements are unique, then theorem-2
can be applied.
Diffstat (limited to 'CheckInsert.agda')
0 files changed, 0 insertions, 0 deletions