constructors-cause-matching-loops.dfy(10,9): Info: Selected triggers: {Succ(s)}
 Rejected triggers:
   {f(s)} (may loop with "f(Succ(s))")
   {f(Succ(s))} (more specific than {Succ(s)})

Dafny program verifier finished with 3 verified, 0 errors