Plan na piąte laboratorium z Coqa

1. Zadania na typy zależne z coqITP2015-course4.v 

a) definicje 
b) dowody używające transparentnych type-cast


Rozwiązania zadań z poprzednich zajęc są w
Rplist.v
RcoqITP2015-ex4-tuple.v