The general method in Dafny for proving something of the form `forall x :: P(x) ==> Q(x)`

is:

lemma X() ensures forall x :: P(x) ==> Q(x); { forall x | P(x) ensures Q(x); { // prove Q(x) } } |

Reply

The general method in Dafny for proving something of the form `forall x :: P(x) ==> Q(x)`

is:

lemma X() ensures forall x :: P(x) ==> Q(x); { forall x | P(x) ensures Q(x); { // prove Q(x) } } |