generalize/weaken lemma-get-mapMV
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 10:37:42 +0000 (11:37 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 10:37:42 +0000 (11:37 +0100)
commitfb860d5088732548eeaf914f9533763f8ec63db4
tree93d6ac506d157fdeca1e5bb9b0d7c259ea440a92
parentc56c7e2e2395d65afd8242df3f9ab45216ba5733
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.
Bidir.agda