Egor Namakonov

Implemented an instance of `Lookup nat (St * option (L * St)) (trace St L)` for an easy access to `i`th transition in a trace. An example usage included in...

These lemmas are used in the 'relive' project. Most of them are general, except for `LTS_traceE'` which, together with existing `LTS_traceE`, states the equivalence of two LTS trace definitions.