define a more useful version of lemma-just\==nnothing
authorHelmut Grohne <helmut@subdivi.de>
Mon, 14 Jan 2013 12:13:00 +0000 (13:13 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Mon, 14 Jan 2013 12:13:00 +0000 (13:13 +0100)
commit9c2be74a5369c1bdb737a67c7c508cb50c62bd83
tree4b2972936dc6377e2df28b6da3b3485a50296813
parenta01871259837d6e36c580338f6d29ea0b154ed04
define a more useful version of lemma-just\==nnothing

If one had a parameter of type just x \== nothing it could be simply
refuted by case splitting. So the cases where lemma-just\==nnothing was
used always employed trans to combine two results. The new version takes
both results instead.
Bidir.agda
CheckInsert.agda
FinMap.agda