complete the yes part of lemma-checkInsert-generate using inspect
-rw-r--r-- 11 .gitignore
-rw-r--r-- 5091 Bidir.agda