sym result of lemma-lookupM-{i,checkI}nsert-other
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 16 Oct 2014 08:57:31 +0000 (10:57 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 16 Oct 2014 08:57:31 +0000 (10:57 +0200)
commit71c4040262bd1c0ac5962425ee4b3bb3b51cc93b
tree796d7fa99a2f20bdbac3e4cfcb400083d733dc93
parentd2548922c7abb20fee5633be6e654430517555af
sym result of lemma-lookupM-{i,checkI}nsert-other

Typically we have the complex term on the LHS and the simplified term on
the RHS. These lemmata did it otherwise and by symming them, we save two
syms.
CheckInsert.agda
FinMap.agda
Precond.agda