let d_update s (p1, p2, p3) v =
  match apply Th.arr s v with
    | App(Arrays(Update), [a; i; x]) when p1 a && p2 i && p3 x -> (a, i, x)
    | _ -> raise Not_found