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 coqITP2015-ex4-tuple.v (zadanie pochodzi ze strony
https://coq.inria.fr/coq-itp-2015)

2. Zadanie plist.v


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