rewrite lemma-\notin-lookupM-assoc
authorHelmut Grohne <helmut@subdivi.de>
Wed, 9 Jan 2013 22:46:10 +0000 (23:46 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Wed, 9 Jan 2013 23:09:08 +0000 (00:09 +0100)
commit400b30320b90620e47a16f3f1ec4ce3dad37e8b0
tree3ee8e6da83fea41b317b66341bba4b026b3b066e
parent3badfdc549d717824f72b0c1df35c52e00ce6dbf
rewrite lemma-\notin-lookupM-assoc

It can be shortened considerably using lemma-checkInsert-lookupM.
Bidir.agda