diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-23 11:48:54 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-23 11:48:54 +0100 |
| commit | 9cb635bb49c1846da7f9c00cc475b0fac9a2fa42 (patch) | |
| tree | a78b7bc2987a76334da921abcf4165bca727b914 /Precond.agda | |
| parent | 808b8da4b14b087c0dcace71fff3854a17cebe42 (diff) | |
| download | bidiragda-9cb635bb49c1846da7f9c00cc475b0fac9a2fa42.tar.gz | |
show a stronger lemma-checkInsert-restrict
We can actually get semantic equality there without requiring anything
else. Indeed this was already hinted in the BX for free paper that says,
that lemma-1 holds in semantic equality.
Diffstat (limited to 'Precond.agda')
0 files changed, 0 insertions, 0 deletions