proposition: Lemma map_subseteq_spec {A} (m1 m2 : M A) : m1 ⊆ m2 ↔ ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
proof: Proof. unfold subseteq, map_subseteq, map_relation. split; intros Hm i; specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)