first attempt to model lemma-1
-rw-r--r-- 11 .gitignore
-rw-r--r-- 3190 Bidir.agda