diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-16 10:57:31 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-16 10:57:31 +0200 |
| commit | 71c4040262bd1c0ac5962425ee4b3bb3b51cc93b (patch) | |
| tree | 796d7fa99a2f20bdbac3e4cfcb400083d733dc93 /Bidir.agda | |
| parent | d2548922c7abb20fee5633be6e654430517555af (diff) | |
| download | bidiragda-71c4040262bd1c0ac5962425ee4b3bb3b51cc93b.tar.gz | |
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.
Diffstat (limited to 'Bidir.agda')
0 files changed, 0 insertions, 0 deletions