diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-24 11:37:42 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-24 11:37:42 +0100 |
| commit | fb860d5088732548eeaf914f9533763f8ec63db4 (patch) | |
| tree | 93d6ac506d157fdeca1e5bb9b0d7c259ea440a92 /FinMap.agda | |
| parent | c56c7e2e2395d65afd8242df3f9ab45216ba5733 (diff) | |
| download | bidiragda-fb860d5088732548eeaf914f9533763f8ec63db4.tar.gz | |
generalize/weaken lemma-get-mapMV
It is now lemma-get-sequenceV and thus no longer applies the free
theorem for the function. Apart making the proof shorter, it also makes
the main use of the free theorem more visible in theorem-2.
Diffstat (limited to 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions