let choose s p x = 
  assert(Term.is_var x);
  let (y, _) = find s x in
    match p y with
      | Some(z) -> z
      | None ->
          let result = ref (Obj.magic 1) in
            try     
              Pre.iter
                (fun y ->
                   match p y with
                     | Some(z) -> 
                         result := z;
                         raise Found
                     | None -> ())
                (inv s y);
              raise Not_found
            with
                Found -> !result