I3: Reflekcja w dużej skali, czyli jak odbijać z rozmachem [TODO]
Chwilowo nic tu nie ma.
Ltac: manipulowanie termami (TODO)
Taktyki dla unifikacji (TODO)
Programowanie funkcyjne w Ltacu (TODO)
Wstawić tutaj przykłady podobne do tych, które opisuje Chlipala. Być
może jakiś większy development, tzn. zaprogramować listy w dwóch
wersjach (zwykłe i zrobione produktem i unitem).