reduce a precondition of lemma-checkInsert-lookupM
authorHelmut Grohne <helmut@subdivi.de>
Thu, 10 Jan 2013 10:09:38 +0000 (11:09 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 10 Jan 2013 10:09:38 +0000 (11:09 +0100)
commitd42ffc9d24adb2b416ff73708ae64c1d4ca50c30
tree48b105cf1f30c79c4a9869d954bdeb9c652e30f2
parent400b30320b90620e47a16f3f1ec4ce3dad37e8b0
reduce a precondition of lemma-checkInsert-lookupM

Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.
Bidir.agda
CheckInsert.agda