predicate P(x:int) { true } 
 
lemma ThereIsMoreThanOneInteger(x:int)
   ensures exists z:int :: z!=x;
{ 
  // can't prove
}
 
lemma NoReallyThereIsMoreThanOneInteger(x:int)
   ensures exists z:int {:trigger P(z)} :: z!=x;
{ 
  assert P(x+1);
  // can prove
}