Generalize `map_relation` and `map_included` / Add `map_Forall2`.

map_Forall and the big ops in Iris also take the key, so this makes map_relation consistent with that.

This also allowed me to add map_Forall2 (defined using map_relation) in a way that is consistent with map_Forall.

This change is not backwards compatible, but I expect little breakage. map_relation is mostly used internally to define (⊆), map_disjoint, map_agree. And aside from a Decision instance there is very little theory about map_relation.