Enable `map_Forall2` to be used in nested inductive relations

This MR allows definitions like the following, whereas they were previously rejected by the positivity checker:

Inductive gtest_rel `{Countable K} : relation (gtest K) :=
  | GTest_rel ts1 ts2 :
     map_Forall2 (λ _, gtest_rel) ts1 ts2 → gtest_rel (GTest ts1) (GTest ts2).

Note that map_Forall2 has only recently been added, see !564 (merged). Hence there is no CHANGELOG entry, but I will announce the break in an @ to iris users.

added 1 commit

• 5e36b905 - Also add a test for `map_Forall`.

Compare with previous version

LGTM, thanks!

mentioned in commit 2dd41ab5

merged

@iris-users If you already using the recently added map_Forall2, this might affect you. Otherwise not.