define combine : (fn <T,U> ((fn T -> Option<U>), (fn T -> Option<U>)) -> (fn T -> Option<U>)) = generic T, U {
      fun 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)))

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

define empty_map : (fn <T,U> T -> Option<U>) = generic T, U {
      fun k:T {
        @none<U>
      }
    }

define flip : (fn <T,U,V> (fn (T, U) -> V) -> (fn (U, T) -> V)) = generic T, U, V {
      fun f {
        fun x, y {
          f(y, x)
        }
      }
    }

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

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

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

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

define update : (fn <T,U> ((fn T -> U), T, U) -> (fn T -> U)) = generic T, U {
      fun 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 x ≠ y then update(f, x, v)(y) = f(y))))

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

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)))