phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_relations.v *)
Lemma max_suffix_fst_suffix l1 l2 : (max_suffix l1 l2).2 `suffix_of` l1.
Proof. eexists. apply max_suffix_fst. Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_fst_suffix_alt l1 l2 k1 k2 k3 :
    max_suffix l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
Proof. eexists. eauto using max_suffix_fst_alt. Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_snd l1 l2 :
    l2 = (max_suffix l1 l2).1.2 ++ (max_suffix l1 l2).2.
Proof.
    rewrite <-(reverse_involutive l2) at 1.
    rewrite (max_prefix_snd (reverse l1) (reverse l2)). unfold max_suffix.
    destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    by rewrite reverse_app.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_snd_alt l1 l2 k1 k2 k3 :
    max_suffix l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
Proof.
    intro. pose proof (max_suffix_snd l1 l2).
    by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_snd_suffix l1 l2 : (max_suffix l1 l2).2 `suffix_of` l2.
Proof. eexists. apply max_suffix_snd. Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_snd_suffix_alt l1 l2 k1 k2 k3 :
    max_suffix l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
Proof. eexists. eauto using max_suffix_snd_alt. Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_max l1 l2 k :
    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` (max_suffix l1 l2).2.
Proof.
    generalize (max_prefix_max (reverse l1) (reverse l2)).
    rewrite !suffix_prefix_reverse. unfold max_suffix.
    destruct (max_prefix (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    rewrite reverse_involutive. auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_max_alt l1 l2 k1 k2 k3 k :
    max_suffix l1 l2 = (k1, k2, k3) →
    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
Proof.
    intro. pose proof (max_suffix_max l1 l2 k).
    by destruct (max_suffix l1 l2) as [[]?]; simplify_eq.
  Qed.
(* stdpp/list_relations.v *)
Lemma max_suffix_max_snoc l1 l2 k1 k2 k3 x1 x2 :
    max_suffix l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
Proof.
    intros Hl ->. destruct (suffix_cons_not x2 k3).
    eapply max_suffix_max_alt; eauto.
    - rewrite (max_suffix_fst_alt _ _ _ _ _ Hl).
      by apply (suffix_app [x2]), suffix_app_r.
    - rewrite (max_suffix_snd_alt _ _ _ _ _ Hl).
      by apply (suffix_app [x2]), suffix_app_r.
  Qed.
(* stdpp/list_relations.v *)
(* ** Properties of the [sublist] predicate *)
Lemma sublist_length l1 l2 : l1 `sublist_of` l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with arith. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_nil_l l : [] `sublist_of` l.
Proof. induction l; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_nil_r l : l `sublist_of` [] ↔ l = [].
Proof. split; [by inv 1|]. intros ->. constructor. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app l1 l2 k1 k2 :
  l1 `sublist_of` l2 → k1 `sublist_of` k2 → l1 ++ k1 `sublist_of` l2 ++ k2.
Proof. induction 1; simpl; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_inserts_l k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_inserts_r k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` l2 ++ k.
Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_cons_r x l k :
  l `sublist_of` x :: k ↔ l `sublist_of` k ∨ ∃ l', l = x :: l' ∧ l' `sublist_of` k.
Proof. split; [inv 1; eauto|]. intros [?|(?&->&?)]; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_cons_l x l k :
  x :: l `sublist_of` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist_of` k2.
Proof.
  split.
  - intros Hlk. induction k as [|y k IH]; inv Hlk.
    + eexists [], k. by repeat constructor.
    + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1), k2.
  - intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app_r l k1 k2 :
  l `sublist_of` k1 ++ k2 ↔
    ∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
Proof.
  split.
  - revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
    { eexists [], l. by repeat constructor. }
    rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst.
    + destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst.
      exists l1, l2. auto using sublist_cons.
    + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
      exists (y :: l1), l2. auto using sublist_skip.
  - intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app_l l1 l2 k :
  l1 ++ l2 `sublist_of` k ↔
    ∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
Proof.
  split.
  - revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
    { eexists [], k. by repeat constructor. }
    rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst.
    destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst.
    exists (k1 ++ x :: h1), h2. rewrite <-(assoc_L (++)).
    auto using sublist_inserts_l, sublist_skip.
  - intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2.
Proof.
  induction k as [|y k IH]; simpl; [done |].
  rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_eq; eauto].
  rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
  apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist_of` l2 ++ k → l1 `sublist_of` l2.
Proof.
  revert l1 l2. induction k as [|y k IH]; intros l1 l2.
  { by rewrite !(right_id_L [] (++)). }
  intros. opose proof* (IH (l1 ++ [_]) (l2 ++ [_])) as Hl12.
  { by rewrite <-!(assoc_L (++)). }
  rewrite sublist_app_l in Hl12. destruct Hl12 as (k1&k2&E&?&Hk2).
  destruct k2 as [|z k2] using rev_ind; [inv Hk2|].
  rewrite (assoc_L (++)) in E; simplify_list_eq.
  eauto using sublist_inserts_r.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app_cons_r x l k1 k2 :
  l `sublist_of` k1 ++ x :: k2 ↔
    l `sublist_of` k1 ++ k2 ∨
    ∃ l1 l2, l = l1 ++ x :: l2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
Proof.
  split.
  - intros (l1 & l2 & -> & ? & [?|(l1'&->&?)]%sublist_cons_r)%sublist_app_r;
      by eauto 10 using sublist_app.
  - intros [(l1 & l1' & -> & ? & ?)%sublist_app_r|(l1 & l2 & -> & ? & ?)].
    + by apply sublist_app, sublist_cons.
    + by apply sublist_app, sublist_skip.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_app_cons_l x l1 l2 k :
  l1 ++ x :: l2 `sublist_of` k ↔
    ∃ k1 k2, k = k1 ++ x :: k2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
Proof.
  split.
  - intros (k1 & k2 & -> & ? & (k1' & k2' & -> & ?)%sublist_cons_l)%sublist_app_l.
    exists (k1 ++ k1'), k2'. rewrite !(assoc_L (++)).
    eauto using sublist_inserts_r.
  - intros (k1 & k2 & -> & ? & ?). by apply sublist_app, sublist_skip.
Qed.
(* stdpp/list_relations.v *)
Instance : PartialOrder (@sublist A).
Proof.
  split; [split|].
  - intros l. induction l; constructor; auto.
  - intros l1 l2 l3 Hl12. revert l3. induction Hl12.
    + auto using sublist_nil_l.
    + intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
      eauto using sublist_inserts_l, sublist_skip.
    + intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
      eauto using sublist_inserts_l, sublist_cons.
  - intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
    induction Hl12 as [| |??? Hl12]; f_equal/=; auto with arith.
    apply sublist_length in Hl12. lia.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_take l i : take i l `sublist_of` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_r. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_drop l i : drop i l `sublist_of` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_l. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_delete l i : delete i l `sublist_of` l.
Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_foldr_delete l js : foldr delete l js `sublist_of` l.
Proof.
  induction js as [|i js IH]; simpl; [done |].
  trans (foldr delete l js); auto using sublist_delete.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_alt l1 l2 : l1 `sublist_of` l2 ↔ ∃ js, l1 = foldr delete l2 js.
Proof.
  split; [|intros [js ->]; apply sublist_foldr_delete].
  intros Hl12. cut (∀ k, ∃ js, k ++ l1 = foldr delete (k ++ l2) js).
  { intros help. apply (help []). }
  induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
  - by eexists [].
  - destruct (IH (k ++ [x])) as [js His]. exists js.
    by rewrite <-!(assoc_L (++)) in His.
  - destruct (IH k) as [js His]. exists (js ++ [length k]).
    rewrite fold_right_app. simpl. by rewrite delete_middle.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_subseteq l1 l2 : l1 `sublist_of` l2 → l1 ⊆ l2.
Proof. intros [js ->]%sublist_alt x. apply list_elem_of_foldr_delete_inv. Qed.
(* stdpp/list_relations.v *)
Lemma elem_of_sublist l1 l2 x : x ∈ l1 → l1 `sublist_of` l2 → x ∈ l2.
Proof. intros. by eapply sublist_subseteq. Qed.
(* stdpp/list_relations.v *)
Lemma singleton_sublist_l l x :
  [x] `sublist_of` l ↔ x ∈ l.
Proof.
  split.
  - intros Hl. eapply elem_of_sublist, Hl. by apply list_elem_of_singleton.
  - intros (l1&l2&->)%list_elem_of_split.
    apply sublist_inserts_l, sublist_skip, sublist_nil_l.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_NoDup l1 l2 :
  NoDup l2 → l1 `sublist_of` l2 → NoDup l1.
Proof.
  intros Hdup. revert l1.
  induction Hdup; inv 1; try constructor; eauto using elem_of_sublist.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_filter P `{! ∀ x : A, Decision (P x)} l :
  filter P l `sublist_of` l.
Proof.
  induction l as [|x l IHl]; [done|]. rewrite filter_cons.
  destruct (decide (P x)); auto using sublist_skip, sublist_cons.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_filter_mono P `{!∀ x : A, Decision (P x)} l1 l2 :
  l1 `sublist_of` l2 →
  filter P l1 `sublist_of` filter P l2.
Proof.
  induction 1; rewrite ?filter_nil, ?filter_cons;
    repeat case_decide; eauto using sublist.
Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_sublist l1 l2 l3 :
  l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3.
Proof.
  intros Hl1l2. revert l3.
  induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2].
  - intros l3. by exists l3.
  - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
    destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4).
    split.
    + by apply sublist_inserts_l, sublist_skip.
    + by rewrite Hl4.
  - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
    rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst.
    exists (l3' ++ y :: l5' ++ x :: l5''). split.
    + by do 2 apply sublist_inserts_l, sublist_skip.
    + by rewrite !Permutation_middle, Permutation_swap.
  - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
    destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
    split; [done|]. etrans; eauto.
Qed.
(* stdpp/list_relations.v *)
Lemma sublist_Permutation l1 l2 l3 :
  l1 `sublist_of` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist_of` l3.
Proof.
  intros Hl1l2 Hl2l3. revert l1 Hl1l2.
  induction Hl2l3 as [|x l2 l3 ? IH|x y l2|l2 l2' l3 ? IH1 ? IH2].
  - intros l1. by exists l1.
  - intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
    { destruct (IH l1) as (l4&?&?); trivial.
      exists l4. split.
      - done.
      - by constructor. }
    destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
    split; [ by constructor | by constructor ].
  - intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
    { exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
      destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
    rewrite sublist_cons_r in Hl1. destruct Hl1 as [?|(l1''&?&?)]; subst.
    + exists (y :: l1'). by repeat constructor.
    + exists (x :: y :: l1''). by repeat constructor.
  - intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
    destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''.
    split; [|done]. etrans; eauto.
Qed.
(* stdpp/list_relations.v *)
(* Properties of the [submseteq] predicate *)
Lemma submseteq_length l1 l2 : l1 ⊆+ l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with lia. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_nil_l l : [] ⊆+ l.
Proof. induction l; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_nil_r l : l ⊆+ [] ↔ l = [].
Proof.
  split; [|intros ->; constructor].
  intros Hl. apply submseteq_length in Hl. destruct l; simpl in *; auto with lia.
Qed.
(* stdpp/list_relations.v *)
Instance : PreOrder (@submseteq A).
Proof.
  split.
  - intros l. induction l; constructor; auto.
  - red. apply submseteq_trans.
Qed.
(* stdpp/list_relations.v *)
Lemma Permutation_submseteq l1 l2 : l1 ≡ₚ l2 → l1 ⊆+ l2.
Proof. induction 1; econstructor; eauto. Qed.
(* stdpp/list_relations.v *)
Lemma sublist_submseteq l1 l2 : l1 `sublist_of` l2 → l1 ⊆+ l2.
Proof. induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_Permutation l1 l2 : l1 ⊆+ l2 → ∃ k, l2 ≡ₚ l1 ++ k.
Proof.
  induction 1 as
    [|x y l ? [k Hk]| |x l1 l2 ? [k Hk]|l1 l2 l3 ? [k Hk] ? [k' Hk']].
  - by eexists [].
  - exists k. by rewrite Hk.
  - eexists []. rewrite (right_id_L [] (++)). by constructor.
  - exists (x :: k). by rewrite Hk, Permutation_middle.
  - exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
Qed.
(* stdpp/list_relations.v *)
Instance : Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@submseteq A).
Proof.
  intros l1 l2 ? k1 k2 ?. split; intros.
  - trans l1; [by apply Permutation_submseteq|].
    trans k1; [done|]. by apply Permutation_submseteq.
  - trans l2; [by apply Permutation_submseteq|].
    trans k2; [done|]. by apply Permutation_submseteq.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_length_Permutation l1 l2 :
  l1 ⊆+ l2 → length l2 ≤ length l1 → l1 ≡ₚ l2.
Proof.
  intros Hsub Hlen. destruct (submseteq_Permutation l1 l2) as [[|??] Hk]; auto.
  - by rewrite Hk, (right_id_L [] (++)).
  - rewrite Hk, length_app in Hlen. simpl in *; lia.
Qed.
(* stdpp/list_relations.v *)
Instance : AntiSymm (≡ₚ) (@submseteq A).
Proof.
  intros l1 l2 ??.
  apply submseteq_length_Permutation; auto using submseteq_length.
Qed.
(* stdpp/list_relations.v *)
Lemma elem_of_submseteq l k x : x ∈ l → l ⊆+ k → x ∈ k.
Proof. intros ? [l' ->]%submseteq_Permutation. apply elem_of_app; auto. Qed.
(* stdpp/list_relations.v *)
Lemma lookup_submseteq l k i x :
  l !! i = Some x →
  l ⊆+ k →
  ∃ j, k !! j = Some x.
Proof.
  intros Hsub Hlook.
  eapply list_elem_of_lookup_1, elem_of_submseteq;
    eauto using list_elem_of_lookup_2.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_take l i : take i l ⊆+ l.
Proof. auto using sublist_take, sublist_submseteq. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_drop l i : drop i l ⊆+ l.
Proof. auto using sublist_drop, sublist_submseteq. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_delete l i : delete i l ⊆+ l.
Proof. auto using sublist_delete, sublist_submseteq. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_foldr_delete l js : foldr delete l js `sublist_of` l.
Proof. auto using sublist_foldr_delete, sublist_submseteq. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_sublist_l l1 l3 : l1 ⊆+ l3 ↔ ∃ l2, l1 `sublist_of` l2 ∧ l2 ≡ₚ l3.
Proof.
  split.
  { intros Hl13. elim Hl13; clear l1 l3 Hl13.
    - by eexists [].
    - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
    - intros x y l. exists (y :: x :: l). by repeat constructor.
    - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
    - intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
      destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
      exists l3'. split; etrans; eauto. }
  intros (l2&?&?).
  trans l2; auto using sublist_submseteq, Permutation_submseteq.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_sublist_r l1 l3 :
  l1 ⊆+ l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist_of` l3.
Proof.
  rewrite submseteq_sublist_l.
  split; intros (l2&?&?); eauto using sublist_Permutation, Permutation_sublist.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_inserts_l k l1 l2 : l1 ⊆+ l2 → l1 ⊆+ k ++ l2.
Proof. induction k; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_inserts_r k l1 l2 : l1 ⊆+ l2 → l1 ⊆+ l2 ++ k.
Proof. rewrite (comm (++)). apply submseteq_inserts_l. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_skips_l k l1 l2 : l1 ⊆+ l2 → k ++ l1 ⊆+ k ++ l2.
Proof. induction k; try constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_skips_r k l1 l2 : l1 ⊆+ l2 → l1 ++ k ⊆+ l2 ++ k.
Proof. rewrite !(comm (++) _ k). apply submseteq_skips_l. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_app l1 l2 k1 k2 : l1 ⊆+ l2 → k1 ⊆+ k2 → l1 ++ k1 ⊆+ l2 ++ k2.
Proof. trans (l1 ++ k2); auto using submseteq_skips_l, submseteq_skips_r. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_cons_r x l k :
  l ⊆+ x :: k ↔ l ⊆+ k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' ⊆+ k.
Proof.
  split.
  - rewrite submseteq_sublist_r. intros (l'&E&Hl').
    rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst.
    + left. rewrite E. eauto using sublist_submseteq.
    + right. eauto using sublist_submseteq.
  - intros [?|(?&E&?)]; [|rewrite E]; by constructor.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_cons_l x l k : x :: l ⊆+ k ↔ ∃ k', k ≡ₚ x :: k' ∧ l ⊆+ k'.
Proof.
  split.
  - rewrite submseteq_sublist_l. intros (l'&Hl'&E).
    rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst.
    exists (k1 ++ k2). split; eauto using submseteq_inserts_l, sublist_submseteq.
    by rewrite Permutation_middle.
  - intros (?&E&?). rewrite E. by constructor.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_app_r l k1 k2 :
  l ⊆+ k1 ++ k2 ↔ ∃ l1 l2, l ≡ₚ l1 ++ l2 ∧ l1 ⊆+ k1 ∧ l2 ⊆+ k2.
Proof.
  split.
  - rewrite submseteq_sublist_r. intros (l'&E&Hl').
    rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
    exists l1, l2. eauto using sublist_submseteq.
  - intros (?&?&E&?&?). rewrite E. eauto using submseteq_app.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_app_l l1 l2 k :
  l1 ++ l2 ⊆+ k ↔ ∃ k1 k2, k ≡ₚ k1 ++ k2 ∧ l1 ⊆+ k1 ∧ l2 ⊆+ k2.
Proof.
  split.
  - rewrite submseteq_sublist_l. intros (l'&Hl'&E).
    rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
    exists k1, k2. split; [done|]. eauto using sublist_submseteq.
  - intros (?&?&E&?&?). rewrite E. eauto using submseteq_app.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
Proof.
  induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l.
  intros (?&E%(inj (cons y))&?). apply IH. by rewrite E.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_app_inv_r l1 l2 k : l1 ++ k ⊆+ l2 ++ k → l1 ⊆+ l2.
Proof. rewrite <-!(comm (++) k). apply submseteq_app_inv_l. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_cons_middle x l k1 k2 : l ⊆+ k1 ++ k2 → x :: l ⊆+ k1 ++ x :: k2.
Proof. rewrite <-Permutation_middle. by apply submseteq_skip. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_app_middle l1 l2 k1 k2 :
  l2 ⊆+ k1 ++ k2 → l1 ++ l2 ⊆+ k1 ++ l1 ++ k2.
Proof.
  rewrite !(assoc (++)), (comm (++) k1 l1), <-(assoc_L (++)).
  by apply submseteq_skips_l.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_middle l k1 k2 : l ⊆+ k1 ++ l ++ k2.
Proof. by apply submseteq_inserts_l, submseteq_inserts_r. Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_submseteq l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l ⊆+ k.
Proof.
  intros Hl. revert k. induction Hl as [|x l Hx ? IH].
  { intros k Hk. by apply submseteq_nil_l. }
  intros k Hlk. destruct (list_elem_of_split k x) as (l1&l2&?); subst.
  { apply Hlk. by constructor. }
  rewrite <-Permutation_middle. apply submseteq_skip, IH.
  intros y Hy. rewrite elem_of_app.
  specialize (Hlk y). rewrite elem_of_app, !elem_of_cons in Hlk.
  by destruct Hlk as [?|[?|?]]; subst; eauto.
Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_Permutation l k : NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → l ≡ₚ k.
Proof.
  intros. apply (anti_symm submseteq); apply NoDup_submseteq; naive_solver.
Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_insert l1 l2 i j x y :
  l1 !! i = Some x →
  l2 !! j = Some x →
  l1 ⊆+ l2 →
  (<[i := y]> l1) ⊆+ (<[j := y]> l2).
Proof.
  intros ?? Hsub.
  rewrite !insert_take_drop,
    <-!Permutation_middle by eauto using lookup_lt_Some.
  rewrite <-(take_drop_middle l1 i x), <-(take_drop_middle l2 j x),
    <-!Permutation_middle in Hsub by done.
  by apply submseteq_skip, (submseteq_app_inv_l _ _ [x]).
Qed.
(* stdpp/list_relations.v *)
Lemma singleton_submseteq_l l x :
  [x] ⊆+ l ↔ x ∈ l.
Proof.
  split.
  - intros Hsub. eapply elem_of_submseteq; [|done].
    apply list_elem_of_singleton. done.
  - intros (l1&l2&->)%list_elem_of_split.
    apply submseteq_cons_middle, submseteq_nil_l.
Qed.
(* stdpp/list_relations.v *)
Lemma singleton_submseteq x y :
  [x] ⊆+ [y] ↔ x = y.
Proof. rewrite singleton_submseteq_l. apply list_elem_of_singleton. Qed.
(* stdpp/list_relations.v *)
Lemma submseteq_inj l1 l2 :
  l1 ⊆+ l2 ↔ ∃ f : nat → nat, Inj (=) (=) f ∧ ∀ i : nat, l1 !! i = l2 !! f i.
Proof.
  split.
  - induction 1 as [|x l1 l2 _ [f [??]]|x y l|x l1 l2 _ [f [??]]
                    |l1 l2 l3 _ [f [? Hf]] _ [g [? Hg]]].
    + exists id; split; [apply _|done].
    + exists (λ i, match i with 0 => 0 | S i => S (f i) end); split.
      * by intros [|i] [|j] ?; simplify_eq/=.
      * intros [|i]; simpl; auto.
    + exists (λ i, match i with 0 => 1 | 1 => 0 | _ => i end); split.
      * intros [|[|i]] [|[|j]]; congruence.
      * by intros [|[|i]].
    + exists (S ∘ f). split; [apply _|]. done.
    + exists (g ∘ f); split; [apply _|]. intros i; simpl. by rewrite <-Hg, <-Hf.
  - intros (f & Hf & Hl). revert l2 f Hf Hl.
    induction l1 as [|x l1 IH]; intros l2 f Hf Hl; [apply submseteq_nil_l|].
    rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl).
    pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1).
    apply submseteq_skip, (IH _ g).
    + unfold g. intros i j Hg.
      repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia.
      apply (inj S), (inj f); lia.
    + intros i. unfold g. destruct (lt_eq_lt_dec _ _) as [[?|?]|?].
      * by rewrite list_lookup_delete_lt, <-Hl.
      * simplify_eq.
      * rewrite list_lookup_delete_ge, <-Nat.sub_succ_l by lia; simpl.
        by rewrite Nat.sub_0_r, <-Hl.
Qed.
(* stdpp/list_relations.v *)
Fixpoint elem_of_or_Permutation x l :
      (x ∉ l) + { k | l ≡ₚ x :: k } :=
    match l with
    | [] => inl _
    | y :: l =>
       if decide (x = y) then inr (l ↾ _) else
       match elem_of_or_Permutation x l return _ with
       | inl _ => inl _ | inr (k ↾ _) => inr ((y :: k) ↾ _)
       end
    end.
Next Obligation. inv 2. Qed.
(* stdpp/list_relations.v *)
Instance submseteq_dec : RelDecision (@submseteq A) :=
    fix go l1 l2 :=
    match l1 with
    | [] => left _
    | x :: l1 =>
       match elem_of_or_Permutation x l2 return _ with
       | inl _ => right _
       | inr (l2 ↾ _) => cast_if (go l1 l2)
       end
    end.
Next Obligation. intros _ l1 l2 _. apply submseteq_nil_l. Qed.
(* stdpp/list_relations.v *)
Instance Permutation_dec : RelDecision (≡ₚ@{A}).
Proof using Type*.
    refine (λ l1 l2, cast_if_and
      (decide (l1 ⊆+ l2)) (decide (length l2 ≤ length l1)));
      [by apply submseteq_length_Permutation
      |abstract (intros He; by rewrite He in *)..].
  Defined.
(* stdpp/list_relations.v *)
(* ** Properties of the [Forall] and [Exists] predicate *)
Lemma Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) :
  ∀ l, {Forall P l} + {Exists Q l}.
Proof.
 refine (
  fix go l :=
  match l return {Forall P l} + {Exists Q l} with
  | [] => left _
  | x :: l => cast_if_and (dec x) (go l)
  end); clear go; intuition.
Defined.
(* stdpp/list_relations.v *)
(* Export the Coq stdlib constructors under different names,
because we use [Forall_nil] and [Forall_cons] for a version with a biimplication. *)
Definition Forall_nil_2
:= @Forall_nil A.
(* stdpp/list_relations.v *)
Definition Forall_cons_2
:= @Forall_cons A.
(* stdpp/list_relations.v *)
Instance Forall_proper:
  Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.