rewrite lemma-1 using propositional equality
-rw-r--r-- 11 .gitignore
-rw-r--r-- 5020 Bidir.agda