Representing lists ds in tamrin

[Choro Ulan uulu]

Dear Tamrin Prover Maintainers, 

For my university project i need to understand how to 

- give tamarin the opportunity to reveal the ith element in a list

- push an element to a list (for example a key)

Could you please explain how to do that in tamarin way? 

Thanks in advance and kind regards,

Choro