generalize lemma-insert-same to arbitrary Setoids
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 16 Jan 2014 10:32:12 +0000 (11:32 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 16 Jan 2014 10:32:12 +0000 (11:32 +0100)
commit48a000f3dc05a9117a9b72e250569c204a4d1371
tree538e2b674eec4b9424683f0c0192ca2e8b31dcdb
parent2c37e0c2f32b4c6b5c121827a4abddf7fc1dd7e0
generalize lemma-insert-same to arbitrary Setoids

The general idea is to enable bff to use arbitrary DecSetoids.
 * assoc needs to learn about DecSetoid
 * checkInsert needs to learn about DecSetoid
 * InsertionResult needs to learn about Setoid
 * Parameters to InsertionResult.same become weaker
 * lemma-checkInsert-restrict should work with weaker same
 * lemma-insert-same needs to learn about Setoid
CheckInsert.agda
FinMap.agda
Generic.agda