rewrite lemma-map-lookupM-assoc
authorHelmut Grohne <helmut@subdivi.de>
Tue, 9 Apr 2013 19:00:14 +0000 (21:00 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 9 Apr 2013 19:00:14 +0000 (21:00 +0200)
commitd296080717675ebd3bc62498465cc4f59a13326f
treea9316eb50131840f8cc1b46c41a1f1f2e37aa62c
parent9b158c066d8801b6bf4bfb007702a076b017efd3
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.
Bidir.agda