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