list.v

  | [], _ => left (prefix_of_nil _)
  | _, [] => right (prefix_of_nil_not _ _)
  | x :: l1, y :: l2 =>
    match decide_rel (=) x y with
    | left Exy =>
      match go l1 l2 with
      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
      | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
      end
    | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
    end
  end.

Section prefix_ops.
  Context `{∀ x y, Decision (x = y)}.

  Lemma max_prefix_of_fst l1 l2 :
    l1 = snd (max_prefix_of l1 l2) ++ fst (fst (max_prefix_of l1 l2)).
  Proof.
    revert l2. induction l1; intros [|??]; simpl;
      repeat case_decide; simpl; f_equal; auto.
  Qed.
  Lemma max_prefix_of_fst_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
  Proof.
    intro. pose proof (max_prefix_of_fst l1 l2).
    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_prefix_of_fst_prefix l1 l2 :
    snd (max_prefix_of l1 l2) `prefix_of` l1.
  Proof. eexists. apply max_prefix_of_fst. Qed.
  Lemma max_prefix_of_fst_prefix_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1, k2, k3) → k3 `prefix_of` l1.
  Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.

  Lemma max_prefix_of_snd l1 l2 :
    l2 = snd (max_prefix_of l1 l2) ++ snd (fst (max_prefix_of l1 l2)).
  Proof.
    revert l2. induction l1; intros [|??]; simpl;
      repeat case_decide; simpl; f_equal; auto.
  Qed.
  Lemma max_prefix_of_snd_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
  Proof.
    intro. pose proof (max_prefix_of_snd l1 l2).
    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_prefix_of_snd_prefix l1 l2 :
    snd (max_prefix_of l1 l2) `prefix_of` l2.
  Proof. eexists. apply max_prefix_of_snd. Qed.
  Lemma max_prefix_of_snd_prefix_alt l1 l2 k1 k2 k3 :
    max_prefix_of l1 l2 = (k1,k2,k3) → k3 `prefix_of` l2.
  Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.

  Lemma max_prefix_of_max l1 l2 k :
    k `prefix_of` l1 → k `prefix_of` l2 →
    k `prefix_of` snd (max_prefix_of l1 l2).
  Proof.
    intros [l1' ?] [l2' ?]. subst.
    by induction k; simpl; repeat case_decide; simpl;
      auto using prefix_of_nil, prefix_of_cons.
  Qed.
  Lemma max_prefix_of_max_alt l1 l2 k1 k2 k3 k :
    max_prefix_of l1 l2 = (k1,k2,k3) →
    k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
  Proof.
    intro. pose proof (max_prefix_of_max l1 l2 k).
    by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
  Qed.

  Lemma max_prefix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
    max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠ x2.
  Proof.
    intros Hl ?. subst. destruct (prefix_of_snoc_not k3 x2).
    eapply max_prefix_of_max_alt; eauto.
    * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
      apply prefix_of_app, prefix_of_cons, prefix_of_nil.
    * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
      apply prefix_of_app, prefix_of_cons, prefix_of_nil.
  Qed.
End prefix_ops.

Lemma prefix_suffix_reverse l1 l2 :
  l1 `prefix_of` l2 ↔ reverse l1 `suffix_of` reverse l2.
Proof.
  split; intros [k E]; exists (reverse k).
  * by rewrite E, reverse_app.
  * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Qed.
Lemma suffix_prefix_reverse l1 l2 :
  l1 `suffix_of` l2 ↔ reverse l1 `prefix_of` reverse l2.
Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.

Lemma suffix_of_nil l : [] `suffix_of` l.
Proof. exists l. by rewrite (right_id_L [] (++)). Qed.
Lemma suffix_of_nil_inv l : l `suffix_of` [] → l = [].
Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
Lemma suffix_of_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Proof. by intros [[] ?]. Qed.
Lemma suffix_of_snoc l1 l2 x :
  l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [x].
Proof. intros [k E]. exists k. subst. by rewrite (associative_L (++)). Qed.
Lemma suffix_of_snoc_alt x y l1 l2 :
  x = y → l1 `suffix_of` l2 → l1 ++ [x] `suffix_of` l2 ++ [y].
Proof. intro. subst. apply suffix_of_snoc. Qed.

Lemma suffix_of_app l1 l2 k : l1 `suffix_of` l2 → l1 ++ k `suffix_of` l2 ++ k.
Proof. intros [k' E]. exists k'. subst. by rewrite (associative_L (++)). Qed.
Lemma suffix_of_app_alt l1 l2 k1 k2 :
  k1 = k2 → l1 `suffix_of` l2 → l1 ++ k1 `suffix_of` l2 ++ k2.
Proof. intro. subst. apply suffix_of_app. Qed.

Lemma suffix_of_snoc_inv_1 x y l1 l2 :
  l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
Proof.
  intros [k' E]. rewrite (associative_L (++)) in E. by simplify_list_equality.
Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 :
  l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite (associative_L (++)) in E.
  by simplify_list_equality.
Qed.
Lemma suffix_of_app_inv l1 l2 k :
  l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
Proof.
  intros [k' E]. exists k'. rewrite (associative_L (++)) in E.
  by simplify_list_equality.
Qed.

Lemma suffix_of_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof.
  intros [k ?]. exists (k ++ [x]). subst. by rewrite <-(associative_L (++)).
Qed.
Lemma suffix_of_app_l l1 l2 l3 : l3 ++ l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof.
  intros [k ?]. exists (k ++ l3). subst. by rewrite <-(associative_L (++)).
Qed.
Lemma suffix_of_cons_r l1 l2 x : l1 `suffix_of` l2 → l1 `suffix_of` x :: l2.
Proof. intros [k ?]. exists (x :: k). by subst. Qed.
Lemma suffix_of_app_r l1 l2 l3 : l1 `suffix_of` l2 → l1 `suffix_of` l3 ++ l2.
Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite (associative_L _). Qed.

Lemma suffix_of_cons_inv l1 l2 x y :
  x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
Proof.
  intros [[|? k] E]; [by left |].
  right. simplify_equality. by apply suffix_of_app_r.
Qed.

Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof. intros [??]. subst. rewrite app_length. lia. Qed.
Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
Proof. intros [??]. discriminate_list_equality. Qed.

Global Instance suffix_of_dec `{∀ x y, Decision (x = y)} l1 l2 :
  Decision (l1 `suffix_of` l2).
Proof.
  refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
   abstract (by rewrite suffix_prefix_reverse).
Defined.

Section max_suffix_of.
  Context `{∀ x y, Decision (x = y)}.

  Lemma max_suffix_of_fst l1 l2 :
    l1 = fst (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
  Proof.
    rewrite <-(reverse_involutive l1) at 1.
    rewrite (max_prefix_of_fst (reverse l1) (reverse l2)). unfold max_suffix_of.
    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    by rewrite reverse_app.
  Qed.
  Lemma max_suffix_of_fst_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
  Proof.
    intro. pose proof (max_suffix_of_fst l1 l2).
    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_suffix_of_fst_suffix l1 l2 :
    snd (max_suffix_of l1 l2) `suffix_of` l1.
  Proof. eexists. apply max_suffix_of_fst. Qed.
  Lemma max_suffix_of_fst_suffix_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1, k2, k3) → k3 `suffix_of` l1.
  Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.

  Lemma max_suffix_of_snd l1 l2 :
    l2 = snd (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
  Proof.
    rewrite <-(reverse_involutive l2) at 1.
    rewrite (max_prefix_of_snd (reverse l1) (reverse l2)).
    unfold max_suffix_of.
    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    by rewrite reverse_app.
  Qed.
  Lemma max_suffix_of_snd_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
  Proof.
    intro. pose proof (max_suffix_of_snd l1 l2).
    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
  Qed.
  Lemma max_suffix_of_snd_suffix l1 l2 :
    snd (max_suffix_of l1 l2) `suffix_of` l2.
  Proof. eexists. apply max_suffix_of_snd. Qed.
  Lemma max_suffix_of_snd_suffix_alt l1 l2 k1 k2 k3 :
    max_suffix_of l1 l2 = (k1,k2,k3) → k3 `suffix_of` l2.
  Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.

  Lemma max_suffix_of_max l1 l2 k :
    k `suffix_of` l1 → k `suffix_of` l2 →
     k `suffix_of` snd (max_suffix_of l1 l2).
  Proof.
    generalize (max_prefix_of_max (reverse l1) (reverse l2)).
    rewrite !suffix_prefix_reverse. unfold max_suffix_of.
    destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
    rewrite reverse_involutive. auto.
  Qed.
  Lemma max_suffix_of_max_alt l1 l2 k1 k2 k3 k :
    max_suffix_of l1 l2 = (k1, k2, k3) →
    k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
  Proof.
    intro. pose proof (max_suffix_of_max l1 l2 k).
    by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
  Qed.

  Lemma max_suffix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
    max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠ x2.
  Proof.
    intros Hl ?. subst. destruct (suffix_of_cons_not x2 k3).
    eapply max_suffix_of_max_alt; eauto.
    * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
      by apply (suffix_of_app [x2]), suffix_of_app_r.
    * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
      by apply (suffix_of_app [x2]), suffix_of_app_r.
  Qed.
End max_suffix_of.

(** ** Properties of the [sublist] predicate *)
Lemma sublist_length l1 l2 : l1 `sublist` l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with arith. Qed.

Lemma sublist_nil_l l : [] `sublist` l.
Proof. induction l; try constructor; auto. Qed.
Lemma sublist_nil_r l : l `sublist` [] ↔ l = [].
Proof. split. by inversion 1. intros. subst. constructor. Qed.

Lemma sublist_app l1 l2 k1 k2 :
  l1 `sublist` l2 → k1 `sublist` k2 → l1 ++ k1 `sublist` l2 ++ k2.
Proof. induction 1; simpl; try constructor; auto. Qed.
Lemma sublist_inserts_l k l1 l2 : l1 `sublist` l2 → l1 `sublist` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma sublist_inserts_r k l1 l2 : l1 `sublist` l2 → l1 `sublist` l2 ++ k.
Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.

Lemma sublist_cons_r x l k :
  l `sublist` x :: k ↔ l `sublist` k ∨ ∃ l', l = x :: l' ∧ l' `sublist` k.
Proof.
  split. inversion 1; eauto. intros [?|(?&?&?)]; subst; constructor; auto.
Qed.
Lemma sublist_cons_l x l k :
  x :: l `sublist` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist` k2.
Proof.
  split.
  * intros Hlk. induction k as [|y k IH]; inversion Hlk.
    + eexists [], k. by repeat constructor.
    + destruct IH as (k1&k2&?&?); subst; auto. by exists (y :: k1) k2.
  * intros (k1&k2&?&?). subst. by apply sublist_inserts_l, sublist_skip.
Qed.

Lemma sublist_app_r l k1 k2 :
  l `sublist` k1 ++ k2 ↔
    ∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist` k1 ∧ l2 `sublist` 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_insert.
    + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
      exists (y :: l1) l2. auto using sublist_skip.
  * intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_l l1 l2 k :
  l1 ++ l2 `sublist` k ↔
    ∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist` k1 ∧ l2 `sublist` 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 <-(associative_L (++)).
    auto using sublist_inserts_l, sublist_skip.
  * intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
Proof.
  induction k as [|y k IH]; simpl; [done |].
  rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_equality; eauto].
  rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
  apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_insert.
Qed.
Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist` l2 ++ k → l1 `sublist` l2.
Proof.
  revert l1 l2. induction k as [|y k IH]; intros l1 l2.
  { by rewrite !(right_id_L [] (++)). }
  intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
  { by rewrite <-!(associative_L (++)). }
  rewrite sublist_app_l in Hl12. destruct Hl12 as (k1&k2&E&?&Hk2).
  destruct k2 as [|z k2] using rev_ind; [inversion Hk2|].
  rewrite (associative_L (++)) in E. simplify_list_equality.
  eauto using sublist_inserts_r.
Qed.

Global 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_insert.
  * intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
    induction Hl12; simpl in *; f_equal; auto with arith.
    apply sublist_length in Hl12. lia.
Qed.

Lemma sublist_take l i : take i l `sublist` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_r. Qed.
Lemma sublist_drop l i : drop i l `sublist` l.
Proof. rewrite <-(take_drop i l) at 2. by apply sublist_inserts_l. Qed.
Lemma sublist_delete l i : delete i l `sublist` l.
Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
Lemma sublist_delete_list l is : delete_list is l `sublist` l.
Proof.
  induction is as [|i is IH]; simpl; [done |].
  transitivity (delete_list is l); auto using sublist_delete.
Qed.

Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = delete_list is l2.
Proof.
  split.
  * intros Hl12. cut (∀ k, ∃ is, k ++ l1 = delete_list is (k ++ l2)).
    { intros help. apply (help []). }
    induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
    + by eexists [].
    + destruct (IH (k ++ [x])) as [is His]. exists is.
      by rewrite <-!(associative_L (++)) in His.
    + destruct (IH k) as [is His]. exists (is ++ [length k]).
      unfold delete_list. rewrite fold_right_app. simpl.
      by rewrite delete_middle.
  * intros [is ?]. subst. apply sublist_delete_list.
Qed.

Lemma Permutation_sublist l1 l2 l3 :
  l1 ≡ₚ l2 → l2 `sublist` l3 → ∃ l4, l1 `sublist` 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. etransitivity; eauto.
Qed.
Lemma sublist_Permutation l1 l2 l3 :
  l1 `sublist` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist` 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]. etransitivity; eauto.
Qed.

(** Properties of the [contains] predicate *)
Lemma contains_length l1 l2 : l1 `contains` l2 → length l1 ≤ length l2.
Proof. induction 1; simpl; auto with lia. Qed.
Lemma contains_nil_l l : [] `contains` l.
Proof. induction l; constructor; auto. Qed.
Lemma contains_nil_r l : l `contains` [] ↔ l = [].
Proof.
  split; [|intros; subst; constructor].
  intros Hl. apply contains_length in Hl. destruct l; simpl in *; auto with lia.
Qed.

Global Instance: PreOrder (@contains A).
Proof.
  split.
  * intros l. induction l; constructor; auto.
  * red. apply contains_trans.
Qed.

Lemma Permutation_contains l1 l2 : l1 ≡ₚ l2 → l1 `contains` l2.
Proof. induction 1; econstructor; eauto. Qed.
Lemma sublist_contains l1 l2 : l1 `sublist` l2 → l1 `contains` l2.
Proof. induction 1; constructor; auto. Qed.
Lemma contains_Permutation_alt l1 l2 :
  length l2 ≤ length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
Proof.
  intros Hl21 Hl12. revert Hl21. elim Hl12; clear l1 l2 Hl12; simpl.
  * constructor.
  * constructor; auto with lia.
  * constructor; auto with lia.
  * intros x l1 l2 ? IH ?. feed specialize IH; [lia|].
    apply Permutation_length in IH. lia.
  * intros l1 l2 l3 Hl12 ? Hl23 ?.
    apply contains_length in Hl12. apply contains_length in Hl23.
    transitivity l2; auto with lia.
Qed.
Lemma contains_Permutation l1 l2 :
  length l2 = length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
Proof. intro. apply contains_Permutation_alt. lia. Qed.

Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@contains A).
Proof.
  intros l1 l2 ? k1 k2 ?. split; intros.
  * transitivity l1. by apply Permutation_contains.
    transitivity k1. done. by apply Permutation_contains.
  * transitivity l2. by apply Permutation_contains.
    transitivity k2. done. by apply Permutation_contains.
Qed.
Global Instance: AntiSymmetric (≡ₚ) (@contains A).
Proof. red. auto using contains_Permutation_alt, contains_length. Qed.

Lemma contains_take l i : take i l `contains` l.
Proof. auto using sublist_take, sublist_contains. Qed.
Lemma contains_drop l i : drop i l `contains` l.
Proof. auto using sublist_drop, sublist_contains. Qed.
Lemma contains_delete l i : delete i l `contains` l.
Proof. auto using sublist_delete, sublist_contains. Qed.
Lemma contains_delete_list l is : delete_list is l `sublist` l.
Proof. auto using sublist_delete_list, sublist_contains. Qed.

Lemma contains_sublist_l l1 l3 :
  l1 `contains` l3 ↔ ∃ l2, l1 `sublist` 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; etransitivity; eauto. }
  intros (l2&?&?).
  transitivity l2; auto using sublist_contains, Permutation_contains.
Qed.
Lemma contains_sublist_r l1 l3 :
  l1 `contains` l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist` l3.
Proof.
  rewrite contains_sublist_l.
  split; intros (l2&?&?); eauto using sublist_Permutation, Permutation_sublist.
Qed.

Lemma contains_inserts_l k l1 l2 : l1 `contains` l2 → l1 `contains` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma contains_inserts_r k l1 l2 : l1 `contains` l2 → l1 `contains` l2 ++ k.
Proof. rewrite (commutative (++)). apply contains_inserts_l. Qed.
Lemma contains_skips_l k l1 l2 : l1 `contains` l2 → k ++ l1 `contains` k ++ l2.
Proof. induction k; try constructor; auto. Qed.
Lemma contains_skips_r k l1 l2 : l1 `contains` l2 → l1 ++ k `contains` l2 ++ k.
Proof. rewrite !(commutative (++) _ k). apply contains_skips_l. Qed.
Lemma contains_app l1 l2 k1 k2 :
  l1 `contains` l2 → k1 `contains` k2 → l1 ++ k1 `contains` l2 ++ k2.
Proof.
  transitivity (l1 ++ k2); auto using contains_skips_l, contains_skips_r.
Qed.

Lemma contains_cons_r x l k :
  l `contains` x :: k ↔ l `contains` k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' `contains` k.
Proof.
  split.
  * rewrite contains_sublist_r. intros (l'&E&Hl').
    rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst.
    + left. rewrite E. eauto using sublist_contains.
    + right. eauto using sublist_contains.
  * intros [?|(?&E&?)]; [|rewrite E]; by constructor.
Qed.
Lemma contains_cons_l x l k :
  x :: l `contains` k ↔ ∃ k', k ≡ₚ x :: k' ∧ l `contains` k'.
Proof.
  split.
  * rewrite contains_sublist_l. intros (l'&Hl'&E).
    rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst.
    exists (k1 ++ k2). split; eauto using contains_inserts_l, sublist_contains.
    by rewrite Permutation_middle.
  * intros (?&E&?). rewrite E. by constructor.
Qed.
Lemma contains_app_r l k1 k2 :
  l `contains` k1 ++ k2 ↔ ∃ l1 l2,
    l ≡ₚ l1 ++ l2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
  split.
  * rewrite contains_sublist_r. intros (l'&E&Hl').
    rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
    exists l1 l2. eauto using sublist_contains.
  * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_l l1 l2 k :
  l1 ++ l2 `contains` k ↔ ∃ k1 k2,
    k ≡ₚ k1 ++ k2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
  split.
  * rewrite contains_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_contains.
  * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_inv_l l1 l2 k :
  k ++ l1 `contains` k ++ l2 → l1 `contains` l2.
Proof.
  induction k as [|y k IH]; simpl; [done |].
  rewrite contains_cons_l. intros (?&E&?).
  apply Permutation_cons_inv in E. apply IH. by rewrite E.
Qed.
Lemma contains_app_inv_r l1 l2 k :
  l1 ++ k `contains` l2 ++ k → l1 `contains` l2.
Proof.
  revert l1 l2. induction k as [|y k IH]; intros l1 l2.
  { by rewrite !(right_id_L [] (++)). }
  intros. feed pose proof (IH (l1 ++ [y]) (l2 ++ [y])) as Hl12.
  { by rewrite <-!(associative_L (++)). }
  rewrite contains_app_l in Hl12. destruct Hl12 as (k1&k2&E1&?&Hk2).
  rewrite contains_cons_l in Hk2. destruct Hk2 as (k2'&E2&?).
  rewrite E2, (Permutation_cons_append k2'), (associative_L (++)) in E1.
  apply Permutation_app_inv_r in E1. rewrite E1. eauto using contains_inserts_r.
Qed.
Lemma contains_cons_middle x l k1 k2 :
  l `contains` k1 ++ k2 → x :: l `contains` k1 ++ x :: k2.
Proof. rewrite <-Permutation_middle. by apply contains_skip. Qed.
Lemma contains_app_middle l1 l2 k1 k2 :
  l2 `contains` k1 ++ k2 → l1 ++ l2 `contains` k1 ++ l1 ++ k2.
Proof.
  rewrite !(associative (++)), (commutative (++) k1 l1), <-(associative_L (++)).
  by apply contains_skips_l.
Qed.
Lemma contains_middle l k1 k2 : l `contains` k1 ++ l ++ k2.
Proof. by apply contains_inserts_l, contains_inserts_r. Qed.

Lemma Permutation_alt l1 l2 :
  l1 ≡ₚ l2 ↔ length l1 = length l2 ∧ l1 `contains` l2.
Proof.
  split.
  * intros Hl. by rewrite Hl.
  * intros [??]. auto using contains_Permutation.
Qed.

Section contains_dec.
  Context `{∀ x y, Decision (x = y)}.

  Lemma list_remove_Permutation l1 l2 k1 x :
    l1 ≡ₚ l2 → list_remove x l1 = Some k1 →
    ∃ k2, list_remove x l2 = Some k2 ∧ k1 ≡ₚ k2.
  Proof.
    intros Hl. revert k1.
    induction Hl as [|y l1 l2 ? IH|y1 y2 l|l1 l2 l3 ? IH1 ? IH2];
      simpl; intros k1 Hk1.
    * done.
    * case_decide; simplify_equality; eauto.
      destruct (list_remove x l1) as [l|] eqn:?; simplify_equality.
      destruct (IH l) as (?&?&?); simplify_option_equality; eauto.
    * repeat case_decide; simplify_option_equality;
        eauto using Permutation_swap.
    * destruct (IH1 k1) as (k2&?&?); trivial.
      destruct (IH2 k2) as (k3&?&?); trivial.
      exists k3. split; eauto. by transitivity k2.
  Qed.

  Lemma list_remove_Some l k x : list_remove x l = Some k → l ≡ₚ x :: k.
  Proof.
    revert k. induction l as [|y l IH]; simpl; intros k ?; [done |].
    case_decide; simplify_option_equality; [done|].
    by rewrite Permutation_swap, <-IH.
  Qed.
  Lemma list_remove_Some_inv l k x :
    l ≡ₚ x :: k → ∃ k', list_remove x l = Some k' ∧ k ≡ₚ k'.
  Proof.
    intros. destruct (list_remove_Permutation (x :: k) l k x) as (k'&?&?).
    * done.
    * simpl; by case_decide.
    * by exists k'.
  Qed.

  Lemma list_remove_list_contains l1 l2 :
    l1 `contains` l2 ↔ is_Some (list_remove_list l1 l2).
  Proof.
    rewrite is_Some_alt. split.
    * revert l2. induction l1 as [|x l1 IH]; simpl.
      { intros l2 _. by exists l2. }
      intros l2. rewrite contains_cons_l. intros (k&Hk&?).
      destruct (list_remove_Some_inv l2 k x) as (k2&?&Hk2); trivial.
      simplify_option_equality. apply IH. by rewrite <-Hk2.
    * intros [k Hk]. revert l2 k Hk.
      induction l1 as [|x l1 IH]; simpl; intros l2 k.
      { intros. apply contains_nil_l. }
      destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_equality.
      rewrite contains_cons_l. eauto using list_remove_Some.
  Qed.

  Global Instance contains_dec l1 l2 : Decision (l1 `contains` l2).
  Proof.
   refine (cast_if (decide (is_Some (list_remove_list l1 l2))));
    abstract (rewrite list_remove_list_contains; tauto).
  Defined.
  Global Instance Permutation_dec l1 l2 : Decision (l1 ≡ₚ l2).
  Proof.
   refine (cast_if_and
    (decide (length l1 = length l2)) (decide (l1 `contains` l2)));
    abstract (rewrite Permutation_alt; tauto).
  Defined.
End contains_dec.
End general_properties.

(** ** Properties of the [same_length] predicate *)
Instance: ∀ A, Reflexive (@same_length A A).
Proof. intros A l. induction l; constructor; auto. Qed.
Instance: ∀ A, Symmetric (@same_length A A).
Proof. induction 1; constructor; auto. Qed.

Section same_length.
  Context {A B : Type}.
  Implicit Types l : list A. Implicit Types k : list B.

  Lemma same_length_length_1 l k : l `same_length` k → length l = length k.
  Proof. induction 1; simpl; auto. Qed.
  Lemma same_length_length_2 l k : length l = length k → l `same_length` k.
  Proof.
    revert k. induction l; intros [|??]; try discriminate;
      constructor; auto with arith.
  Qed.
  Lemma same_length_length l k : l `same_length` k ↔ length l = length k.
  Proof. split; auto using same_length_length_1, same_length_length_2. Qed.

  Lemma same_length_lookup l k i :
    l `same_length` k → is_Some (l !! i) → is_Some (k !! i).
  Proof.
    rewrite same_length_length. setoid_rewrite lookup_lt_length.
    intros E. by rewrite E.
  Qed.

  Lemma same_length_take l k n :
    l `same_length` k → take n l `same_length` take n k.
  Proof. intros Hl. revert n; induction Hl; intros [|n]; constructor; auto. Qed.
  Lemma same_length_drop l k n :
    l `same_length` k → drop n l `same_length` drop n k.
  Proof.
    intros Hl. revert n; induction Hl; intros [|]; simpl; try constructor; auto.
  Qed.
  Lemma same_length_resize l k x y n : resize n x l `same_length` resize n y k.
  Proof. apply same_length_length. by rewrite !resize_length. Qed.
End same_length.

(** ** Properties of the [Forall] and [Exists] predicate *)
Section Forall_Exists.
  Context {A} (P : A → Prop).

  Definition Forall_nil_2 := @Forall_nil A.
  Definition Forall_cons_2 := @Forall_cons A.

  Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
  Proof.
    split.
    * induction 1; inversion 1; subst; auto.
    * intros Hin. induction l; constructor.
      + apply Hin. constructor.
      + apply IHl. intros ??. apply Hin. by constructor.
  Qed.

  Lemma Forall_nil : Forall P [] ↔ True.
  Proof. done. Qed.
  Lemma Forall_cons_1 x l : Forall P (x :: l) → P x ∧ Forall P l.
  Proof. by inversion 1. Qed.
  Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall P l.
  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
  Lemma Forall_singleton x : Forall P [x] ↔ P x.
  Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
  Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H ?]. induction H; simpl; intuition.
  Qed.
  Lemma Forall_true l : (∀ x, P x) → Forall P l.
  Proof. induction l; auto. Qed.
  Lemma Forall_impl l (Q : A → Prop) :
    Forall P l → (∀ x, P x → Q x) → Forall Q l.
  Proof. intros H ?. induction H; auto. Defined.

  Global Instance Forall_proper:
    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
  Proof. split; subst; induction 1; constructor; firstorder. Qed.

  Lemma Forall_iff l (Q : A → Prop) :
    (∀ x, P x ↔ Q x) → Forall P l ↔ Forall Q l.
  Proof. intros H. apply Forall_proper. red. apply H. done. Qed.

  Lemma Forall_delete l i : Forall P l → Forall P (delete i l).
  Proof. intros H. revert i. by induction H; intros [|i]; try constructor. Qed.
  Lemma Forall_lookup l : Forall P l ↔ ∀ i x, l !! i = Some x → P x.
  Proof.
    rewrite Forall_forall. setoid_rewrite elem_of_list_lookup. naive_solver.
  Qed.
  Lemma Forall_lookup_1 l i x : Forall P l → l !! i = Some x → P x.
  Proof. rewrite Forall_lookup. eauto. Qed.
  Lemma Forall_lookup_2 l : (∀ i x, l !! i = Some x → P x) → Forall P l.
  Proof. by rewrite Forall_lookup. Qed.

  Lemma Forall_alter f l i :
    Forall P l → (∀ x, l !! i = Some x → P x → P (f x)) →
    Forall P (alter f i l).
  Proof.
    intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.

  Lemma Forall_replicate n x : P x → Forall P (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.
  Lemma Forall_replicate_eq n (x : A) : Forall (=x) (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.

  Lemma Forall_take n l : Forall P l → Forall P (take n l).
  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
  Lemma Forall_drop n l : Forall P l → Forall P (drop n l).
  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
  Lemma Forall_resize n x l : P x → Forall P l → Forall P (resize n x l).
  Proof.
    intros ? Hl. revert n.
    induction Hl; intros [|?]; simpl; auto using Forall_replicate.
  Qed.
  Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
  Proof.
    split.
    * induction 1 as [x|y ?? IH].
      + exists x. split. constructor. done.
      + destruct IH as [x [??]]. exists x. split. by constructor. done.
    * intros [x [Hin ?]]. induction l.
      + by destruct (not_elem_of_nil x).
      + inversion Hin; subst. by left. right; auto.
  Qed.
  Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
  Proof. inversion 1; intuition trivial. Qed.
  Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H|H]; [induction H | induction l1]; simpl; intuition.
  Qed.

  Global Instance Exists_proper:
    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A).
  Proof. split; subst; (induction 1; [left|right]; firstorder auto). Qed.

  Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.
  Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
  Proof. induction 1; inversion_clear 1; contradiction. Qed.

  Context {dec : ∀ x, Decision (P x)}.

  Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (not ∘ P) l}.
  Proof.
   refine (
    match l with
    | [] => left _
    | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
    end); clear Forall_Exists_dec; abstract intuition.
  Defined.

  Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
  Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.

  Global Instance Forall_dec l : Decision (Forall P l) :=
    match Forall_Exists_dec l with
    | left H => left H
    | right H => right (Exists_not_Forall _ H)
    end.

  Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (not ∘ P) l}.
  Proof.
   refine (
    match l with
    | [] => right _
    | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
    end); clear Exists_Forall_dec; abstract intuition.
  Defined.

  Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
  Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.

  Global Instance Exists_dec l : Decision (Exists P l) :=
    match Exists_Forall_dec l with
    | left H => left H
    | right H => right (Forall_not_Exists _ H)
    end.
End Forall_Exists.

Lemma Forall_swap {A B} (Q : A → B → Prop) l1 l2 :
  Forall (λ y, Forall (Q y) l1) l2 ↔ Forall (λ x, Forall (flip Q x) l2) l1.
Proof. repeat setoid_rewrite Forall_forall. simpl. split; eauto. Qed.

(** ** Properties of the [Forall2] predicate *)
Section Forall2.
  Context {A B} (P : A → B → Prop).

  Lemma Forall2_nil_inv_l k : Forall2 P [] k → k = [].
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_inv_r k : Forall2 P k [] → k = [].
  Proof. by inversion 1. Qed.
  Lemma Forall2_cons_inv l1 l2 x1 x2 :
    Forall2 P (x1 :: l1) (x2 :: l2) → P x1 x2 ∧ Forall2 P l1 l2.
  Proof. by inversion 1. Qed.
  Lemma Forall2_cons_inv_l l1 k x1 :
    Forall2 P (x1 :: l1) k → ∃ x2 l2, P x1 x2 ∧ Forall2 P l1 l2 ∧ k = x2 :: l2.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_inv_r k l2 x2 :
    Forall2 P k (x2 :: l2) → ∃ x1 l1, P x1 x2 ∧ Forall2 P l1 l2 ∧ k = x1 :: l1.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_nil_inv l1 x1 : Forall2 P (x1 :: l1) [] → False.
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_cons_inv l2 x2 : Forall2 P [] (x2 :: l2) → False.
  Proof. by inversion 1. Qed.
  Lemma Forall2_app_inv l1 l2 k1 k2 :
    l1 `same_length` k1 →
    Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l1 k1 ∧ Forall2 P l2 k2.
  Proof. induction 1. done. inversion 1; naive_solver. Qed.
  Lemma Forall2_app_inv_l l1 l2 k :
    Forall2 P (l1 ++ l2) k →
      ∃ k1 k2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ k = k1 ++ k2.
  Proof. revert k. induction l1; simpl; inversion 1; naive_solver. Qed.
  Lemma Forall2_app_inv_r l k1 k2 :
    Forall2 P l (k1 ++ k2) →
      ∃ l1 l2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ l = l1 ++ l2.
  Proof. revert l. induction k1; simpl; inversion 1; naive_solver. Qed.

  Lemma Forall2_length l1 l2 : Forall2 P l1 l2 → length l1 = length l2.
  Proof. induction 1; simpl; auto. Qed.
  Lemma Forall2_same_length l1 l2 : Forall2 P l1 l2 → l1 `same_length` l2.
  Proof. induction 1; constructor; auto. Qed.

  Lemma Forall2_flip l1 l2 : Forall2 P l1 l2 ↔ Forall2 (flip P) l2 l1.
  Proof. split; induction 1; constructor; auto. Qed.
  Lemma Forall2_impl (Q : A → B → Prop) l1 l2 :
    Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2.
  Proof. intros H ?. induction H; auto. Defined.
  Lemma Forall2_unique l k1 k2 :
    Forall2 P l k1 →  Forall2 P l k2 →
    (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) → k1 = k2.
  Proof.
    intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
  Qed.

  Lemma Forall2_Forall_l (Q : A → Prop) l k :
    Forall2 P l k → Forall (λ y, ∀ x, P x y → Q x) k → Forall Q l.
  Proof. induction 1; inversion_clear 1; eauto. Qed.
  Lemma Forall2_Forall_r (Q : B → Prop) l k :
    Forall2 P l k → Forall (λ x, ∀ y, P x y → Q y) l → Forall Q k.
  Proof. induction 1; inversion_clear 1; eauto. Qed.

  Lemma Forall2_lookup_lr l1 l2 i x y :
    Forall2 P l1 l2 → l1 !! i = Some x → l2 !! i = Some y → P x y.
  Proof.
    intros H. revert i. induction H; [done|].
    intros [|?] ??; simpl in *; simplify_equality; eauto.
  Qed.
  Lemma Forall2_lookup_l l1 l2 i x :
    Forall2 P l1 l2 → l1 !! i = Some x → ∃ y, l2 !! i = Some y ∧ P x y.
  Proof.
    intros H. revert i. induction H; [done|].
    intros [|?] ?; simpl in *; simplify_equality; eauto.
  Qed.
  Lemma Forall2_lookup_r l1 l2 i y :
    Forall2 P l1 l2 → l2 !! i = Some y → ∃ x, l1 !! i = Some x ∧ P x y.
  Proof.
    intros H. revert i. induction H; [done|].
    intros [|?] ?; simpl in *; simplify_equality; eauto.
  Qed.
  Lemma Forall2_lookup_2 l1 l2 :
    l1 `same_length` l2 →
    (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → P x y) → Forall2 P l1 l2.
  Proof.
    eauto using Forall2_same_length, Forall2_lookup_lr.
    intros Hl Hlookup. induction Hl as [|????? IH]; constructor.
    * by apply (Hlookup 0).
    * apply IH. intros i. apply (Hlookup (S i)).
  Qed.
  Lemma Forall2_lookup l1 l2 :
    Forall2 P l1 l2 ↔ l1 `same_length` l2 ∧
      (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → P x y).
  Proof.
    split.
    * eauto using Forall2_same_length, Forall2_lookup_lr.
    * intros [??]; eauto using Forall2_lookup_2.
  Qed.
  Lemma Forall2_alter_l f l1 l2 i :
    Forall2 P l1 l2 → (∀ x1 x2,
      l1 !! i = Some x1 → l2 !! i = Some x2 → P x1 x2 → P (f x1) x2) →
    Forall2 P (alter f i l1) l2.
  Proof.
    intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall2_alter_r f l1 l2 i :
    Forall2 P l1 l2 → (∀ x1 x2,
      l1 !! i = Some x1 → l2 !! i = Some x2 → P x1 x2 → P x1 (f x2)) →
    Forall2 P l1 (alter f i l2).
  Proof.
    intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall2_alter f g l1 l2 i :
    Forall2 P l1 l2 → (∀ x1 x2,
      l1 !! i = Some x1 → l2 !! i = Some x2 → P x1 x2 → P (f x1) (g x2)) →
    Forall2 P (alter f i l1) (alter g i l2).
  Proof.
    intros Hl. revert i. induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall2_delete l1 l2 i :
    Forall2 P l1 l2 → Forall2 P (delete i l1) (delete i l2).
  Proof.
    intros Hl12. revert i. induction Hl12; intros [|i]; simpl; intuition.
  Qed.
  Lemma Forall2_replicate_l l n x :
    Forall (P x) l → length l = n → Forall2 P (replicate n x) l.
  Proof.
    intros Hl. revert n.
    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
  Qed.
  Lemma Forall2_replicate_r l n x :
    Forall (flip P x) l → length l = n → Forall2 P l (replicate n x).
  Proof.
    intros Hl. revert n.
    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
  Qed.
  Lemma Forall2_replicate n x1 x2 :
    P x1 x2 → Forall2 P (replicate n x1) (replicate n x2).
  Proof. induction n; simpl; constructor; auto. Qed.
  Lemma Forall2_take l1 l2 n :
    Forall2 P l1 l2 → Forall2 P (take n l1) (take n l2).
  Proof. intros Hl1l2. revert n. induction Hl1l2; intros [|?]; simpl; auto. Qed.
  Lemma Forall2_drop l1 l2 n :
    Forall2 P l1 l2 → Forall2 P (drop n l1) (drop n l2).
  Proof. intros Hl1l2. revert n. induction Hl1l2; intros [|?]; simpl; auto. Qed.
  Lemma Forall2_resize l1 l2 x1 x2 n :
    P x1 x2 → Forall2 P l1 l2 → Forall2 P (resize n x1 l1) (resize n x2 l2).
  Proof.
    intros. rewrite !resize_spec, (Forall2_length l1 l2) by done.
    auto using Forall2_app, Forall2_take, Forall2_replicate.
  Qed.

  Lemma Forall2_resize_ge_l l1 l2 x1 x2 n m :
    P x1 x2 → Forall (flip P x2) l1 → n ≤ m →
    Forall2 P (resize n x1 l1) l2 → Forall2 P (resize m x1 l1) (resize m x2 l2).
  Proof.
    intros. assert (n = length l2).
    { by rewrite <-(Forall2_length (resize n x1 l1) l2), resize_length. }
    rewrite (le_plus_minus n m) by done. subst.
    rewrite !resize_plus, resize_all, drop_all, resize_nil.
    apply Forall2_app; [done |].
    apply Forall2_replicate_r; [| by rewrite resize_length].
    eauto using Forall_resize, Forall_drop.
  Qed.
  Lemma Forall2_resize_ge_r l1 l2 x1 x2 n m :
    P x1 x2 → Forall (P x1) l2 → n ≤ m →
    Forall2 P l1 (resize n x2 l2) → Forall2 P (resize m x1 l1) (resize m x2 l2).
  Proof.
    intros. assert (n = length l1).
    { by rewrite (Forall2_length l1 (resize n x2 l2)), resize_length. }
    rewrite (le_plus_minus n m) by done. subst.
    rewrite !resize_plus, resize_all, drop_all, resize_nil.
    apply Forall2_app; [done |].
    apply Forall2_replicate_l; [| by rewrite resize_length].
    eauto using Forall_resize, Forall_drop.
  Qed.

  Lemma Forall2_transitive {C} (Q : B → C → Prop) (R : A → C → Prop) l1 l2 l3 :
    (∀ x1 x2 x3, P x1 x2 → Q x2 x3 → R x1 x3) →
    Forall2 P l1 l2 → Forall2 Q l2 l3 → Forall2 R l1 l3.
  Proof.
    intros ? Hl1l2. revert l3. induction Hl1l2; inversion_clear 1; eauto.