T:Type, as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i]

By:	(Assert (T:Type, n:, as:T List. n||as||  (i:n. firstn(n;as)[i] = as[i]))) THEN HypBackchain

1

T:Type, n:, as:T List. n||as||  (i:n. firstn(n;as)[i] = as[i])

6 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html