base case of lemma-2
-rw-r--r-- 11 .gitignore
-rw-r--r-- 5149 Bidir.agda