let exists s p x = 
  assert(Term.is_var x);
  let (y, _) = find s x in
    p y || Pre.exists p (inv s y)