Plan na trzecie laboratorium z Coqa:

0. Rozwiązania zadań z poprzedniego labu znajdują się w pliku RcoqITP2015-ex3.v

1. Zrobić dowody do przykładu o kompilacji omawianego na wykładzie
(zadanie pochodzi z CPDT): 
pliki OneSortStackMachine.v, MultiSortStackMachine.v

2. Zadanie plist.v