change lemma-insert-same to work with \== proofs
-rw-r--r-- 11 .gitignore
-rw-r--r-- 5018 Bidir.agda