attempt to prove lemma-1
authorHelmut Grohne <helmut@subdivi.de>
Sun, 22 Jan 2012 15:40:58 +0000 (16:40 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sun, 22 Jan 2012 15:40:58 +0000 (16:40 +0100)
commit2f01bfa8f4580eb0777a66946c62dd5af6f2867c
tree914610edc58a49036e968a81c9f486612a5537d6
parenta511dceb455975ded324c14c10f3cb6f85b95c3d
attempt to prove lemma-1

In order to prove lemma-1 we first show a lemma-insert-same to show that
inserting the same pair twice does not change the FinMapMaye. lemma-1 still
has two goals. In the first goal agda doesn't accept "is-just (f i)". Why?
The second goal is to be shown as absurd.
Bidir.agda