p := λ(: tt Type)(: i U64). (: (
   (match tt (
      ()
      ( (TGround( _ ts )) (set tt (.nth( ts i TAny ))) )
      ( _ () )
   ))
   tt
) Type);

p1 := λ(: tt Type). (: (p( tt 0_u64 )) Type);
p2 := λ(: tt Type). (: (p( tt 1_u64 )) Type);