save a with in lemma-\inn-lookupM-assoc
authorHelmut Grohne <helmut@subdivi.de>
Mon, 17 Sep 2012 20:17:02 +0000 (22:17 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Mon, 17 Sep 2012 20:17:02 +0000 (22:17 +0200)
commit99e4f3024fd5542b6f33ed3b756db6eb97201c39
tree88d72db8cb56f4c82c60044396aa25e0f53b5728
parentdd4bbd5d31c003a054f676b859012105be81394b
save a with in lemma-\inn-lookupM-assoc

Since \negp can be written as i\innis \circ here.
Bidir.agda