Plan na trzecie laboratorium z Coqa:

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

1. Zadanie plist.v

2. Zadanie coqITP2015-ex4-tuple.v (zadanie pochodzi ze strony
https://coq.inria.fr/coq-itp-2015)

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