prove theorem-2 in the presence of delete
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 24 Jan 2014 12:30:39 +0000 (13:30 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 24 Jan 2014 12:30:39 +0000 (13:30 +0100)
commit2d7db0d8c48c41ecef78ef9f18253632a80f4710
tree39252b0237db5e1891da79b3203232abd27d2d14
parent88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907
prove theorem-2 in the presence of delete

The biggest piece of this puzzle was establishing
  get <$> mapMV f v == mapMV f (get v)
provided that the result of mapMV is just something.
lemma-union-not-used lost a "map just", but could be retained in
structure.
Bidir.agda
Generic.agda