proposition: Lemma lookup_submseteq l k i x : l !! i = Some x → l ⊆+ k → ∃ j, k !! j = Some x.
proof: Proof. intros Hsub Hlook. eapply elem_of_list_lookup_1, elem_of_submseteq; eauto using elem_of_list_lookup_2. Qed.
imports: stdpp(options)