prove NoDup_fmap_2_strong

Merged Ralf Jung requested to merge ralf/no-dup-fmap into master

Another lemma that I just needed in Perennial.

Merge request reports