diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-01-22 16:40:58 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-01-22 16:40:58 +0100 |
| commit | 2f01bfa8f4580eb0777a66946c62dd5af6f2867c (patch) | |
| tree | 914610edc58a49036e968a81c9f486612a5537d6 /LiftGet.agda | |
| parent | a511dceb455975ded324c14c10f3cb6f85b95c3d (diff) | |
| download | bidiragda-2f01bfa8f4580eb0777a66946c62dd5af6f2867c.tar.gz | |
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.
Diffstat (limited to 'LiftGet.agda')
0 files changed, 0 insertions, 0 deletions