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