prove assoc-enough in the presence of delete
-rw-r--r-- 11 .gitignore
-rw-r--r-- 1773 BFF.agda
-rw-r--r-- 13027 Bidir.agda
-rw-r--r-- 5031 CheckInsert.agda
-rw-r--r-- 7357 FinMap.agda
-rw-r--r-- 780 FreeTheorems.agda
-rw-r--r-- 3695 Generic.agda
-rw-r--r-- 8400 LiftGet.agda
-rw-r--r-- 7299 Precond.agda