prove the remaining parts of lemma-checkInsert-generate

Introducing the following lemmata:
 * lemma-lookupM-empty : nothing \== lookupM i empty
 * lemma-from-just : just x \== just y -> x \== y
 * lemma-lookupM-insert : just a \== lookupM i (insert i a m)
 * lemma-lookupM-insert-other : \neg (i \== j) ->
   lookupM i m \== lookupM i (insert j a m)
 * lemma-lookupM-generate : just a = lookupM i (generate f is) -> a \== f i

0 files changed, 0 insertions, 0 deletions