prove the remaining parts of lemma-checkInsert-generate
-rw-r--r-- 11 .gitignore
-rw-r--r-- 7752 Bidir.agda