formulate theorem-2
-rw-r--r-- 11 .gitignore
-rw-r--r-- 9070 Bidir.agda
-rw-r--r-- 6500 FinMap.agda