prove mismatch using take_plus_one lemma
-add header files for extracting the specification of equal and mismatch
-add equal_by_mismatch.c
-include listex.gh and call lemma take_plus_one from this file