Stronger induction principle for `map_fold`.

(Based on a proposal by @johannes, see https://mattermost.mpi-sws.org/iris/pl/uosw3r3xx7dhmgz9o4xy7joxpe)

The new induction principle is:

  map_fold_ind {A} (P : M A → Prop) :
    P ∅ →
    (∀ i x m,
      m !! i = None →
      (∀ B (f : K → A → B → B) b,
        map_fold f b (<[i:=x]> m) = f i x (map_fold f b m)) →
      P m →
      P (<[i:=x]> m)) →
    ∀ m, P m;

This induction scheme is like map_ind, but it gives an equality for map_fold for the current element (i/x) without any conditions on f. This is sound because all uses of fold and the induction principle traverse the map in the same way.

• The new scheme implies map_fold_foldr from !565 (closed)
• It also implies the proposed rule map_to_list_cons_inv by @johannes in https://mattermost.mpi-sws.org/iris/pl/drduhw8etirftc7bkwdjhj57fr
• I think the new map_fold_ind is more usable than the old one since you can just do induction m as .. using map_fold_ind. You do not need to revert and manually apply the scheme. Hence I renamed the old scheme into map_fold_weak_ind, which should discourage one from using it.
• Additional bonus: Using the new scheme we can easily prove map_fold_comm_acc(_strong)? without needless side-conditions, making it consistent with the versions of sets and multisets.