Forall_Forall2 should be a different lemma
As discussed in iris!620 (merged), the lemma currently called Forall_Forall2
should really be called Forall_Forall2_diag
, and there could/should be another lemma Forall_Forall2
that's more like big_sepL_sepL2
.