show a stronger lemma-checkInsert-restrict
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 23 Jan 2014 10:48:54 +0000 (11:48 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 23 Jan 2014 10:48:54 +0000 (11:48 +0100)
commit9cb635bb49c1846da7f9c00cc475b0fac9a2fa42
treea78b7bc2987a76334da921abcf4165bca727b914
parent808b8da4b14b087c0dcace71fff3854a17cebe42
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.
Bidir.agda
CheckInsert.agda
FinMap.agda