Function tracked_empty_list_owner 

pub proof fn tracked_empty_list_owner<M: AnyFrameMeta + Repr<MetaSlotSmall>>() -> tracked res : LinkedListOwner<M>

ensures

res.list =~= Seq::<LinkOwner>::empty(),

res.repr_perms =~= Seq::<LinkInnerPerms<M>>::empty(),

res.list_id == 0,

Tracked constructor for a fresh empty list owner.