proposition: Lemma lookup_weaken_None {A} (m1 m2 : M A) i : m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
proof: Proof. rewrite map_subseteq_spec, !eq_None_not_Some. intros Hm2 Hm [??]; destruct Hm2; eauto. Qed.
imports: Coq(Permutation) stdpp(options)