phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_relations.v *)
Instance Exists_proper:
  Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A).
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
Proof.
    split; [induction 1; inv 1; auto|].
    intros Hin; induction l as [|x l IH]; constructor; [apply Hin; constructor|].
    apply IH. intros ??. apply Hin. by constructor.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_nil : Forall P [] ↔ True.
Proof. done. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_cons_1 x l : Forall P (x :: l) → P x ∧ Forall P l.
Proof. by inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall P l.
Proof. split; [by inv 1|]. intros [??]. by constructor. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_singleton x : Forall P [x] ↔ P x.
Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_app_2 l1 l2 : Forall P l1 → Forall P l2 → Forall P (l1 ++ l2).
Proof. induction 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
Proof.
    split; [induction l1; inv 1; naive_solver|].
    intros [??]; auto using Forall_app_2.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_true l : (∀ x, P x) → Forall P l.
Proof. intros ?. induction l; auto. Defined.
(* stdpp/list_relations.v *)
Lemma Forall_impl (Q : A → Prop) l :
    Forall P l → (∀ x, P x → Q x) → Forall Q l.
Proof. intros H ?. induction H; auto. Defined.
(* stdpp/list_relations.v *)
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.
(* stdpp/list_relations.v *)
Lemma Forall_not l : length l ≠ 0 → Forall (not ∘ P) l → ¬Forall P l.
Proof. by destruct 2; inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_and {Q} l : Forall (λ x, P x ∧ Q x) l ↔ Forall P l ∧ Forall Q l.
Proof.
    split; [induction 1; constructor; naive_solver|].
    intros [Hl Hl']; revert Hl'; induction Hl; inv 1; auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_and_l {Q} l : Forall (λ x, P x ∧ Q x) l → Forall P l.
Proof. rewrite Forall_and; tauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_and_r {Q} l : Forall (λ x, P x ∧ Q x) l → Forall Q l.
Proof. rewrite Forall_and; tauto. Qed.
(* stdpp/list_relations.v *)
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.
(* stdpp/list_relations.v *)
Lemma Forall_lookup l : Forall P l ↔ ∀ i x, l !! i = Some x → P x.
Proof.
    rewrite Forall_forall. setoid_rewrite list_elem_of_lookup. naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_lookup_total `{!Inhabited A} l :
    Forall P l ↔ ∀ i, i < length l → P (l !!! i).
Proof. rewrite Forall_lookup. setoid_rewrite list_lookup_alt. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_lookup_1 l i x : Forall P l → l !! i = Some x → P x.
Proof. rewrite Forall_lookup. eauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_lookup_total_1 `{!Inhabited A} l i :
    Forall P l → i < length l → P (l !!! i).
Proof. rewrite Forall_lookup_total. eauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_lookup_2 l : (∀ i x, l !! i = Some x → P x) → Forall P l.
Proof. by rewrite Forall_lookup. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_lookup_total_2 `{!Inhabited A} l :
    (∀ i, i < length l → P (l !!! i)) → Forall P l.
Proof. by rewrite Forall_lookup_total. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_nth d l : Forall P l ↔ ∀ i, i < length l → P (nth i l d).
Proof.
    rewrite Forall_lookup. split.
    - intros Hl ? [x Hl']%lookup_lt_is_Some_2.
      rewrite (nth_lookup_Some _ _ _ _ Hl'). by eapply Hl.
    - intros Hl i x Hl'. specialize (Hl _ (lookup_lt_Some _ _ _ Hl')).
      by rewrite (nth_lookup_Some _ _ _ _ Hl') in Hl.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_reverse l : Forall P (reverse l) ↔ Forall P l.
Proof.
    induction l as [|x l IH]; simpl; [done|].
    rewrite reverse_cons, Forall_cons, Forall_app, Forall_singleton. naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_tail l : Forall P l → Forall P (tail l).
Proof. destruct 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
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.
(* stdpp/list_relations.v *)
Lemma Forall_alter_inv f l i :
    Forall P (alter f i l) → (∀ x, l !! i = Some x → P (f x) → P x) → Forall P l.
Proof.
    revert i. induction l; intros [|?]; simpl;
      inv 1; constructor; eauto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_insert l i x : Forall P l → P x → Forall P (<[i:=x]>l).
Proof. rewrite list_insert_alter; auto using Forall_alter. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_inserts l i k :
    Forall P l → Forall P k → Forall P (list_inserts i k l).
Proof.
    intros Hl Hk; revert i.
    induction Hk; simpl; auto using Forall_insert.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_replicate n x : P x → Forall P (replicate n x).
Proof. induction n; simpl; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_replicate_eq n (x : A) : Forall (x =.) (replicate n x).
Proof using -(P). induction n; simpl; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_take n l : Forall P l → Forall P (take n l).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_drop n l : Forall P l → Forall P (drop n l).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_rev_ind (Q : list A → Prop) :
    Q [] → (∀ x l, P x → Forall P l → Q l → Q (l ++ [x])) →
    ∀ l, Forall P l → Q l.
Proof.
    intros ?? l. induction l using rev_ind; auto.
    rewrite Forall_app, Forall_singleton; intros [??]; auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
Proof.
    split.
    - induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
    - intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
      inv Hin; subst; [left|right]; auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
Proof. inv 1; intuition trivial. Qed.
(* stdpp/list_relations.v *)
Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
Proof.
    split.
    - induction l1; inv 1; naive_solver.
    - intros [H|H]; [induction H | induction l1]; simpl; intuition.
  Qed.
(* stdpp/list_relations.v *)
Lemma Exists_impl (Q : A → Prop) l :
    Exists P l → (∀ x, P x → Q x) → Exists Q l.
Proof. intros H ?. induction H; auto. Defined.
(* stdpp/list_relations.v *)
Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
Proof. induction 1; inv 1; contradiction. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
Proof. induction 1; inv 1; contradiction. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_list_difference `{!EqDecision A} l k :
    Forall P l → Forall P (list_difference l k).
Proof.
    rewrite !Forall_forall.
    intros ? x; rewrite list_elem_of_difference; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_list_union `{!EqDecision A} l k :
    Forall P l → Forall P k → Forall P (list_union l k).
Proof. intros. apply Forall_app; auto using Forall_list_difference. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_list_intersection `{!EqDecision A} l k :
    Forall P l → Forall P (list_intersection l k).
Proof.
    rewrite !Forall_forall.
    intros ? x; rewrite list_elem_of_intersection; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
Proof using Type*. intro. by destruct (Forall_Exists_dec P (not ∘ P) dec l). Qed.
(* stdpp/list_relations.v *)
Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
Proof using Type*.
    by destruct (Forall_Exists_dec (not ∘ P) P
        (λ x : A, swap_if (decide (P x))) l).
  Qed.
(* stdpp/list_relations.v *)
Instance Forall_dec l : Decision (Forall P l)
:=
    match Forall_Exists_dec P (not ∘ P) dec l with
    | left H => left H
    | right H => right (Exists_not_Forall _ H)
    end.
(* stdpp/list_relations.v *)
Instance Exists_dec l : Decision (Exists P l)
:=
    match Forall_Exists_dec (not ∘ P) P (λ x, swap_if (decide (P x))) l with
    | left H => right (Forall_not_Exists _ H)
    | right H => left H
    end.
(* stdpp/list_relations.v *)
Instance Forall_Permutation :
  Proper (pointwise_relation _ (↔) ==> (≡ₚ) ==> (↔)) (@Forall A).
Proof.
  intros P1 P2 HP l1 l2 Hl. rewrite !Forall_forall.
  apply forall_proper; intros x. by rewrite Hl, (HP x).
Qed.
(* stdpp/list_relations.v *)
Instance Exists_Permutation :
  Proper (pointwise_relation _ (↔) ==> (≡ₚ) ==> (↔)) (@Exists A).
Proof.
  intros P1 P2 HP l1 l2 Hl. rewrite !Exists_exists.
  f_equiv; intros x. by rewrite Hl, (HP x).
Qed.
(* stdpp/list_relations.v *)
Lemma head_filter_Some P `{!∀ x : A, Decision (P x)} l x :
  head (filter P l) = Some x →
  ∃ l1 l2, l = l1 ++ x :: l2 ∧ Forall (λ z, ¬P z) l1.
Proof.
  intros Hl. induction l as [|x' l IH]; [done|].
  rewrite filter_cons in Hl. case_decide; simplify_eq/=.
  - exists [], l. repeat constructor.
  - destruct IH as (l1&l2&->&?); [done|].
    exists (x' :: l1), l2. by repeat constructor.
Qed.
(* stdpp/list_relations.v *)
Lemma last_filter_Some P `{!∀ x : A, Decision (P x)} l x :
  last (filter P l) = Some x →
  ∃ l1 l2, l = l1 ++ x :: l2 ∧ Forall (λ z, ¬P z) l2.
Proof.
  rewrite <-(reverse_involutive (filter P l)), last_reverse, <-filter_reverse.
  intros (l1&l2&Heq&Hl)%head_filter_Some.
  exists (reverse l2), (reverse l1).
  rewrite <-(reverse_involutive l), Heq, reverse_app, reverse_cons, <-(assoc_L (++)).
  split; [done|by apply Forall_reverse].
Qed.
(* stdpp/list_relations.v *)
Lemma list_exist_dec P l :
  (∀ x, Decision (P x)) → Decision (∃ x, x ∈ l ∧ P x).
Proof.
  refine (λ _, cast_if (decide (Exists P l))); by rewrite <-Exists_exists.
Defined.
(* stdpp/list_relations.v *)
Lemma list_forall_dec P l :
  (∀ x, Decision (P x)) → Decision (∀ x, x ∈ l → P x).
Proof.
  refine (λ _, cast_if (decide (Forall P l))); by rewrite <-Forall_forall.
Defined.
(* stdpp/list_relations.v *)
Lemma forallb_True (f : A → bool) xs : forallb f xs ↔ Forall f xs.
Proof.
  split.
  - induction xs; naive_solver.
  - induction 1; naive_solver.
Qed.
(* stdpp/list_relations.v *)
Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs.
Proof.
  split.
  - induction xs; naive_solver.
  - induction 1; naive_solver.
Qed.
(* stdpp/list_relations.v *)
Lemma replicate_as_Forall (x : A) n l :
  replicate n x = l ↔ length l = n ∧ Forall (x =.) l.
Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma replicate_as_Forall_2 (x : A) n l :
  length l = n → Forall (x =.) l → replicate n x = l.
Proof. by rewrite replicate_as_Forall. Qed.
(* stdpp/list_relations.v *)
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.
(* stdpp/list_relations.v *)
(* ** Properties of the [Forall2] predicate *)
Lemma Forall_Forall2_diag {A} (Q : A → A → Prop) l :
  Forall (λ x, Q x x) l → Forall2 Q l l.
Proof. induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_forall `{Inhabited A} B C (Q : A → B → C → Prop) l k :
  Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
Proof.
  split; [induction 1; constructor; auto|].
  intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
  - intros z. by oinv Hlk.
  - apply IH. intros z. by oinv Hlk.
Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_same_length {A B} (l : list A) (k : list B) :
  Forall2 (λ _ _, True) l k ↔ length l = length k.
Proof.
  split; [by induction 1; f_equal/=|].
  revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_Forall {A} P (l1 l2 : list A) :
  Forall2 P l1 l2 → Forall (uncurry P) (zip l1 l2).
Proof. induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
(* Export the Coq stdlib constructors under a different name,
because we use [Forall2_nil] and [Forall2_cons] for a version with a biimplication. *)
Definition Forall2_nil_2
:= @Forall2_nil.
(* stdpp/list_relations.v *)
Definition Forall2_cons_2
:= @Forall2_cons.
(* stdpp/list_relations.v *)
Lemma Forall2_length l k : Forall2 P l k → length l = length k.
Proof. by induction 1; f_equal/=. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_length_l l k n : Forall2 P l k → length l = n → length k = n.
Proof. intros ? <-; symmetry. by apply Forall2_length. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_length_r l k n : Forall2 P l k → length k = n → length l = n.
Proof. intros ? <-. by apply Forall2_length. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_true l k : (∀ x y, P x y) → length l = length k → Forall2 P l k.
Proof. rewrite <-Forall2_same_length. induction 2; naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_flip l k : Forall2 (flip P) k l ↔ Forall2 P l k.
Proof. split; induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_trans {C} (Q : B → C → Prop) (R : A → C → Prop) l k lC :
    (∀ x y z, P x y → Q y z → R x z) →
    Forall2 P l k → Forall2 Q k lC → Forall2 R l lC.
Proof. intros ? Hl. revert lC. induction Hl; inv 1; eauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_impl (Q : A → B → Prop) l k :
    Forall2 P l k → (∀ x y, P x y → Q x y) → Forall2 Q l k.
Proof. intros H ?. induction H; auto. Defined.
(* stdpp/list_relations.v *)
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; inv 1; intros; f_equal; eauto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall_Forall2_l l k :
    length l = length k → Forall (λ x, ∀ y, P x y) l → Forall2 P l k.
Proof. rewrite <-Forall2_same_length. induction 1; inv 1; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall_Forall2_r l k :
    length l = length k → Forall (λ y, ∀ x, P x y) k → Forall2 P l k.
Proof. rewrite <-Forall2_same_length. induction 1; inv 1; auto. Qed.
(* stdpp/list_relations.v *)
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; inv 1; eauto. Qed.
(* stdpp/list_relations.v *)
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; inv 1; eauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_nil_inv_l k : Forall2 P [] k → k = [].
Proof. by inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_nil_inv_r l : Forall2 P l [] → l = [].
Proof. by inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_nil : Forall2 P [] [] ↔ True.
Proof. done. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_cons_1 x l y k :
    Forall2 P (x :: l) (y :: k) → P x y ∧ Forall2 P l k.
Proof. by inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_cons_inv_l x l k :
    Forall2 P (x :: l) k → ∃ y k', P x y ∧ Forall2 P l k' ∧ k = y :: k'.
Proof. inv 1; eauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_cons_inv_r l k y :
    Forall2 P l (y :: k) → ∃ x l', P x y ∧ Forall2 P l' k ∧ l = x :: l'.
Proof. inv 1; eauto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_cons_nil_inv x l : Forall2 P (x :: l) [] → False.
Proof. by inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_nil_cons_inv y k : Forall2 P [] (y :: k) → False.
Proof. by inv 1. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_cons x l y k :
    Forall2 P (x :: l) (y :: k) ↔ P x y ∧ Forall2 P l k.
Proof.
    split; [by apply Forall2_cons_1|]. intros []. by apply Forall2_cons_2.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_app_l l1 l2 k :
    Forall2 P l1 (take (length l1) k) → Forall2 P l2 (drop (length l1) k) →
    Forall2 P (l1 ++ l2) k.
Proof. intros. rewrite <-(take_drop (length l1) k). by apply Forall2_app. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_app_r l k1 k2 :
    Forall2 P (take (length k1) l) k1 → Forall2 P (drop (length k1) l) k2 →
    Forall2 P l (k1 ++ k2).
Proof. intros. rewrite <-(take_drop (length k1) l). by apply Forall2_app. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_app_inv l1 l2 k1 k2 :
    length l1 = length k1 →
    Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l1 k1 ∧ Forall2 P l2 k2.
Proof.
    rewrite <-Forall2_same_length. induction 1; inv 1; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
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.
    split; [|intros (?&?&?&?&->); by apply Forall2_app].
    revert k. induction l1; inv 1; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
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.
    split; [|intros (?&?&?&?&->); by apply Forall2_app].
    revert l. induction k1; inv 1; naive_solver.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_tail l k : Forall2 P l k → Forall2 P (tail l) (tail k).
Proof. destruct 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_take l k n : Forall2 P l k → Forall2 P (take n l) (take n k).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_drop l k n : Forall2 P l k → Forall2 P (drop n l) (drop n k).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_lookup l k :
    Forall2 P l k ↔ ∀ i, option_Forall2 P (l !! i) (k !! i).
Proof.
    split; [induction 1; intros [|?]; simpl; try constructor; eauto|].
    revert k. induction l as [|x l IH]; intros [| y k] H.
    - done.
    - oinv (H 0).
    - oinv (H 0).
    - constructor; [by oinv (H 0)|]. apply (IH _ $ λ i, H (S i)).
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_lookup_lr l k i x y :
    Forall2 P l k → l !! i = Some x → k !! i = Some y → P x y.
Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_lookup_l l k i x :
    Forall2 P l k → l !! i = Some x → ∃ y, k !! i = Some y ∧ P x y.
Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_lookup_r l k i y :
    Forall2 P l k → k !! i = Some y → ∃ x, l !! i = Some x ∧ P x y.
Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_same_length_lookup_2 l k :
    length l = length k →
    (∀ i x y, l !! i = Some x → k !! i = Some y → P x y) → Forall2 P l k.
Proof.
    rewrite <-Forall2_same_length. intros Hl Hlookup.
    induction Hl as [|?????? IH]; constructor; [by apply (Hlookup 0)|].
    apply IH. apply (λ i, Hlookup (S i)).
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_same_length_lookup l k :
    Forall2 P l k ↔
      length l = length k ∧
      (∀ i x y, l !! i = Some x → k !! i = Some y → P x y).
Proof.
    naive_solver eauto using Forall2_length,
      Forall2_lookup_lr, Forall2_same_length_lookup_2.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_alter_l f l k i :
    Forall2 P l k →
    (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) y) →
    Forall2 P (alter f i l) k.
Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_alter_r f l k i :
    Forall2 P l k →
    (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P x (f y)) →
    Forall2 P l (alter f i k).
Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_alter f g l k i :
    Forall2 P l k →
    (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) (g y)) →
    Forall2 P (alter f i l) (alter g i k).
Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_insert l k x y i :
    Forall2 P l k → P x y → Forall2 P (<[i:=x]> l) (<[i:=y]> k).
Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_inserts l k l' k' i :
    Forall2 P l k → Forall2 P l' k' →
    Forall2 P (list_inserts i l' l) (list_inserts i k' k).
Proof. intros ? H. revert i. induction H; eauto using Forall2_insert. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_delete l k i :
    Forall2 P l k → Forall2 P (delete i l) (delete i k).
Proof. intros Hl. revert i. induction Hl; intros [|]; simpl; intuition. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_option_list mx my :
    option_Forall2 P mx my → Forall2 P (option_list mx) (option_list my).
Proof. destruct 1; by constructor. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_filter Q1 Q2 `{∀ x, Decision (Q1 x), ∀ y, Decision (Q2 y)} l k:
    (∀ x y, P x y → Q1 x ↔ Q2 y) →
    Forall2 P l k → Forall2 P (filter Q1 l) (filter Q2 k).
Proof.
    intros HP; induction 1 as [|x y l k]; unfold filter; simpl; auto.
    simplify_option_eq by (by rewrite <-(HP x y)); repeat constructor; auto.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_replicate_l k n x :
    length k = n → Forall (P x) k → Forall2 P (replicate n x) k.
Proof. intros <-. induction 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_replicate_r l n y :
    length l = n → Forall (flip P y) l → Forall2 P l (replicate n y).
Proof. intros <-. induction 1; simpl; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_replicate n x y :
    P x y → Forall2 P (replicate n x) (replicate n y).
Proof. induction n; simpl; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_reverse l k : Forall2 P l k → Forall2 P (reverse l) (reverse k).
Proof.
    induction 1; rewrite ?reverse_nil, ?reverse_cons; eauto using Forall2_app.
  Qed.
(* stdpp/list_relations.v *)
Lemma Forall2_last l k : Forall2 P l k → option_Forall2 P (last l) (last k).
Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance Forall2_dec `{dec : ∀ x y, Decision (P x y)} :
    RelDecision (Forall2 P).
Proof.
   refine (
    fix go l k : Decision (Forall2 P l k) :=
    match l, k with
    | [], [] => left _
    | x :: l, y :: k => cast_if_and (decide (P x y)) (go l k)
    | _, _ => right _
    end); clear dec go; abstract first [by constructor | by inv 1].
  Defined.
(* stdpp/list_relations.v *)
Lemma Forall_exists_Forall2_l {A B} (R : A → B → Prop) (l : list A) :
  Forall (λ x, ∃ y, R x y) l ↔ ∃ k, Forall2 R l k.
Proof.
  split.
  - induction 1; naive_solver.
  - intros [k HRlk]. induction HRlk; eauto.
Qed.
(* stdpp/list_relations.v *)
Lemma Forall_exists_Forall2_r {A B} (R : A → B → Prop) (k : list B) :
  Forall (λ y, ∃ x, R x y) k ↔ ∃ l, Forall2 R l k.
Proof. setoid_rewrite Forall2_flip. apply Forall_exists_Forall2_l. Qed.
(* stdpp/list_relations.v *)
Instance : Reflexive R → Reflexive (Forall2 R).
Proof. intros ? l. induction l; by constructor. Qed.
(* stdpp/list_relations.v *)
Instance : Symmetric R → Symmetric (Forall2 R).
Proof. intros. induction 1; constructor; auto. Qed.
(* stdpp/list_relations.v *)
Instance : Transitive R → Transitive (Forall2 R).
Proof. intros ????. apply Forall2_trans. by apply @transitivity. Qed.
(* stdpp/list_relations.v *)
Instance : Equivalence R → Equivalence (Forall2 R).
Proof. split; apply _. Qed.
(* stdpp/list_relations.v *)
Instance : PreOrder R → PreOrder (Forall2 R).
Proof. split; apply _. Qed.
(* stdpp/list_relations.v *)
Instance : AntiSymm (=) R → AntiSymm (=) (Forall2 R).
Proof. induction 2; inv 1; f_equal; auto. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (R ==> Forall2 R ==> Forall2 R) (::).
Proof. by constructor. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (++).
Proof. repeat intro. by apply Forall2_app. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (Forall2 R ==> (=)) length.
Proof. repeat intro. eauto using Forall2_length. Qed.
(* stdpp/list_relations.v *)
Instance : Proper (Forall2 R ==> Forall2 R) tail.
Proof. repeat intro. eauto using Forall2_tail. Qed.