For instance, the behavior of a function last that yields the last element of a list can be specified as follows: for all lists xs and elements e, last xs = e if ∃ys:ys++ = xs.
De exemplu, comportamentul unei funcții care are ultimul element dintr-o listă poate fi specificat după cum urmează: pentru toate listele last xs = e dacă ∃ys:ys++ = xs.