define mapMV via sequenceV
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 10:28:31 +0000 (11:28 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 10:28:31 +0000 (11:28 +0100)
commitc56c7e2e2395d65afd8242df3f9ab45216ba5733
tree0f5769f75738de972093ea4d77f1d3f203d3c4f7
parentd0392d237baa5cb5561ea878fb05ddfb597bba90
define mapMV via sequenceV

This makes a few proofs easier and eliminates the need for sequence-map
entirely.
Bidir.agda
Generic.agda
Precond.agda