proposition: Lemma lookup_weaken_inv {A} (m1 m2 : M A) i x y : m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some y → x = y.
proof: Proof. intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto. congruence. Qed.
imports: Coq(Permutation) stdpp(options)