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

define first : (fn <T,U> Pair<T,U> -> T) = generic T, U {
      fun p:Pair<T,U> {
        switch p {
          case pair(x, y) {
            x
          }
        }
      }
    }

first_pair: (all T:type, U:type, x:T, y:U. first(pair(x, y)) = x)

pair_first_second: (all T:type, U:type. (all p:Pair<T,U>. pair(first(p), second(p)) = p))

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

define second : (fn <T,U> Pair<T,U> -> U) = generic T, U {
      fun p:Pair<T,U> {
        switch p {
          case pair(x, y) {
            y
          }
        }
      }
    }

second_pair: (all T:type, U:type, x:T, y:U. second(pair(x, y)) = y)