proposition: Lemma map_subset_alt {A} (m1 m2 : M A) : m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i).
proof: Proof. rewrite strict_spec_alt. split. - intros [? Heq]; split; [done|]. destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2))) as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists |Hm%(not_Exists_Forall _)]; [eauto|]. destruct Heq; apply (anti_symm (⊆)), map_subseteq_spec; [done|intros i x Hi]. assert (is_Some (m1 !! i)) as [x' ?]. { by apply not_eq_None_Some, (proj1 (Forall_forall _ _) Hm (i,x)), elem_of_map_to_list. } by rewrite <-(lookup_weaken_inv m1 m2 i x' x). - intros [? (i&?&x&?)]; split; [done|]. congruence. Qed.
imports: Coq(Permutation) stdpp(options)