Dokończ dowód poprawności procedury MergeSort prezentowanej na wykładzie.

1. Udowodnij poprawność zawartości (zachowanie elementów listy) dla procedury split.
   Zastanów się nad odpowiednim sposobem dowodzenia indukcyjnego:
   • spróbuj normalnie :)
   • ew. zdefiniuj własny predykat indukcyjny dla list - "co 2 elementy"
   • albo wygeneruj schemat na podstawie definicji funkcji split - polecenie Functional Scheme - i wykorzystaj go za pomocą polecenia functional induction.
2. Udowodnij poprawność zawartości (zachowanie elementów listy) dla całej procedury sortującej MergeSort.
3. Udowodnij poprawność sortowania (właściwa kolejność elementów), kolejno dla funkcji merge, split i MergeSort.