The source project of this merge request has been removed.
Compatibility lemma between big_sepM and big_sepL2 with map_to_list
Simple lemma to convert [∗ map] k↦v ∈ m, φ k v into [∗ list] k;v ∈ lk;lv, φ k v.
Simple lemma to convert [∗ map] k↦v ∈ m, φ k v into [∗ list] k;v ∈ lk;lv, φ k v.