It is possible to write tiggers for particular quantifiers in Dafny programs.

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 } |