let mk_select =
  let select = mk_app (Arrays(Select)) in
    fun is_equal b j ->
      match b with
        | App(Arrays(Create), [a]) ->
            a
        | App(Arrays(Update), [a; i; x]) ->
            (match is_equal i j with
               | Three.Yes ->
                   x
               | Three.No -> 
                   select [a; j]
               | Three.X ->
                   select [b; j])
        | _ ->
            select [b; j]