Big op lemmas `big_op{L,L2,M,M2,S}_intuitionistically_forall`
This MR adds variants of the following lemma for all big ops:
Lemma big_sepL_intuitionistically_forall Φ l :
□ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x) ⊢ [∗ list] k↦x ∈ l, Φ k x.
It also uses these lemmas to simplify a number of existing proofs.
Lastly, it adds the missing lemmas big_sepL2_forall
, big_sepMS_forall
, big_sepMS_impl
, big_sepMS_dup
.