Simplify wptp_recv_strong_normal_adequacy

[paldepind]

The lemma wptp_recv_strong_normal_adequacy quantifies over an argument ns. But, if ns is not the empty list the first assumption is false and the lemma is pretty vacuous.

This PR changes the lemma by, essentially, inlining ns = []. This simplifies the statement, its proof, and the places where the lemma is used.

[RalfJung]

This one is probably for @jtassarotti

[tchajed]

@paldepind sorry for the long delay - would you mind rebasing on top of master? I gave it an attempt but something about wptp_recv_strong_normal_adequacy has changed so that step_fupd2N_wand doesn't directly apply and I can't quite figure out how to adapt the proof.