employ insertionresult in lemma-lookupM-checkInsert
authorHelmut Grohne <helmut@subdivi.de>
Fri, 1 Feb 2013 12:13:01 +0000 (13:13 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 1 Feb 2013 12:13:01 +0000 (13:13 +0100)
commit9b158c066d8801b6bf4bfb007702a076b017efd3
tree5e1c4c42a68c7b449e5a359fdd9386d0966e42da
parentdf1c4f99c384e2e94c1e05ebf79e29947a6f5d83
employ insertionresult in lemma-lookupM-checkInsert
CheckInsert.agda