complete lemma-2 using new property _in-domain-of_
-rw-r--r-- 11 .gitignore
-rw-r--r-- 21619 Bidir.agda
-rw-r--r-- 6487 FinMap.agda