datatype List<T> = Nil | Cons(head: T, tail: List<T>)

// Implement a useful list membership test...
predicate Member<X(==)>(x: X, xs: List<X>)
{
  match xs
  
}

// ... and implement a useful indexing function
function At<X>(xs: List<X>, i: nat): X
{
  xs.head
}