started proving lemma-2
authorHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 16:12:44 +0000 (17:12 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 16:12:44 +0000 (17:12 +0100)
commit5ece23e8705d2ea3128961a24baed6652383b1ad
tree148625bc910dc5687e2da85e3fef493e91ec47be
parent1e2ddab6a91377a939d47e30ed1575b03784a09f
started proving lemma-2

The step case needs two lemmata. One for the head of the resulting map and one
for the tail. The head case is shown using a

lemma-lookupM-assoc : assoc eq (i :: _) (x :: _) == just h ->
  lookupM i h == just x
Bidir.agda