reduce hole in lemma-2
authorHelmut Grohne <helmut@subdivi.de>
Thu, 19 Apr 2012 10:27:00 +0000 (12:27 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 19 Apr 2012 10:27:00 +0000 (12:27 +0200)
commitbf27d0ee5b48bfc843cdc9bd26b163e25a520df4
tree4f72d6783830c967a861f13d301975b0952af256
parentfcf8bd5d0530dd6b05ba5c2931a66171b823e651
reduce hole in lemma-2

Introduce lemma-map-lookupM-assoc. It branches on whether the newly
inserted element is already present. To employ the results of this
branch two new lemmata lemma-\in-lookupM-assoc and
lemma-\notin-lookupM-assoc are used and they need
lemma-lookupM-checkInsert. The remaining hole in lemma-map-lookupM-assoc
targets the case where the checkInsert actually is an insert of a new
element. It probably needs more thinking to get this case right.
Bidir.agda