diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-04-09 21:00:14 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-04-09 21:00:14 +0200 |
| commit | d296080717675ebd3bc62498465cc4f59a13326f (patch) | |
| tree | a9316eb50131840f8cc1b46c41a1f1f2e37aa62c /FinMap.agda | |
| parent | 9b158c066d8801b6bf4bfb007702a076b017efd3 (diff) | |
| download | bidiragda-d296080717675ebd3bc62498465cc4f59a13326f.tar.gz | |
rewrite lemma-map-lookupM-assoc
Indeed the usage of is in two different places can be disentangled. What
we need is that all lookupM succeed. We already know how to express
this: _in-domain-of_. So use a separate list js to map over and require
js in-domain-of h'. This is what the original proof actually did. Just
now we can drop ph' and therefore is and xs. Also
lemma-map-lookupM-insert vanishes, because this generalized form permits
direct induction.
Diffstat (limited to 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions