union Pair<T,U> {
  pair(T,U)
}

fun first<T,U>(p : Pair<T,U>)  {
  switch p {
    case pair(x,y) { x }
  }
}

fun second<T,U>(p : Pair<T,U>) {
  switch p {
    case pair(x,y) { y }
  }
}

fun pairfun<T1,T2,U1,U2>(f : fn T1->T2, g : fn U1->U2) {
  fun p: Pair<T1,U1> {
    pair(f(first(p)), g(second(p)))
  }
}

theorem first_pair: all T:type,U:type, x:T, y:U. first(pair(x,y)) = x
proof
  arbitrary T:type,U:type, x:T, y:U
  expand first.
end
  
theorem second_pair: all T:type,U:type, x:T, y:U. second(pair(x,y)) = y
proof
  arbitrary T:type,U:type, x:T, y:U
  expand second.
end