coq怎么往一个元组里边添加一个元素

问题遇到的现象和发生背景：已知一个多元组的列表Record TData:=
mkTData{
TL: Tasks;
TS: TaskStatus;
TP: priority;
}.
初始化之后怎么往其中添加一条新的数据

求求各位大佬了，小弟毕设卡到这里好几天不知所措了，跪谢