fun operator ∘<T, U, V>(g:(fn U -> V), f:(fn T -> U)) {
  fun x:T {
    g(f(x))
  }
}

fun update<T, U>(f:(fn T -> U), x:T, v:U) {
  fun y:T {
    if y = x then
      v
    else
      f(y)
  }
}

update_eq: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U. update(f, x, v)(x) = v))

update_not_eq: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, y:T. (if not (x = y) then update(f, x, v)(y) = f(y))))

update_shadow: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, w:U. update(update(f, x, v), x, w) = update(f, x, w)))

update_permute: (all T:type, U:type. (all f:(fn T -> U), x:T, v:U, w:U, y:T. (if not (x = y) then update(update(f, x, v), y, w) = update(update(f, y, w), x, v))))

fun empty_map<T, U>(k:T) {
  @none<U>
}

fun domain<T, U>(f:(fn T -> Option<U>)) {
  set_of_pred(fun x:T { switch f(x) { case none { false } case just(y) { true } } })
}

fun restrict<T, U>(f:(fn T -> Option<U>), P:Set<T>) {
  fun x:T {
    if x ∈ P then
      f(x)
    else
      @none<U>
  }
}

fun combine<T, U>(f:(fn T -> Option<U>), g:(fn T -> Option<U>)) {
  fun x:T {
    if f(x) = none then
      g(x)
    else
      f(x)
  }
}

combine_left: (all T:type, U:type, f:(fn T -> Option<U>), g:(fn T -> Option<U>), x:T. (if g(x) = none then combine(f, g)(x) = f(x)))

combine_right: (all T:type, U:type, f:(fn T -> Option<U>), g:(fn T -> Option<U>), x:T. (if f(x) = none then combine(f, g)(x) = g(x)))

restrict_domain: (all T:type, U:type. (all f:(fn T -> Option<U>), P:Set<T>. domain(restrict(f, P)) ⊆ P))

fun flip<T, U, V>(f) {
  fun x, y {
    f(y, x)
  }
}

flip_flip: (all T:type. (all f:(fn T, T -> T). flip(flip(f)) = f))