Enable `map_Forall2` to be used in nested inductive relations
Compare changes
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).