Require Import List.
Import ListNotations.
Require Import StructTact.StructTactics.
Require Import StructTact.ListTactics.
Require Import StructTact.ListUtil.
Require Import StructTact.RemoveAll.
Require Import StructTact.PropUtil.
Require Import FunctionalExtensionality.
Require Import Sumbool.
Require Import Sorting.Permutation.
Require Import Relation_Definitions.
Require Import RelationClasses.

Definition update2 {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (f : A -> A -> B) (x y : A) (v : B) :=
  fun x' y' => if sumbool_and _ _ _ _ (A_eq_dec x x') (A_eq_dec y y') then v else f x' y'.

Fixpoint collate {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (from : A) (f : A -> A -> list B) (ms : list (A * B)) :=
  match ms with
   | [] => f
   | (to, m) :: ms' => collate A_eq_dec from (update2 A_eq_dec f from to (f from to ++ [m])) ms'
  end.

Fixpoint collate_ls {A B : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (s : list A) (f : A -> A -> list B) (to : A) (m : B) :=
  match s with
   | [] => f
   | from :: s' => collate_ls A_eq_dec s' (update2 A_eq_dec f from to (f from to ++ [m])) to m
  end.

Fixpoint filter_rel {A : Type} {rel : relation A} (A_rel_dec : forall x y : A, {rel x y} + {~ rel x y}) (x : A) (l : list A) :=
  match l with
   | [] => []
   | y :: tl => if A_rel_dec x y then y :: filter_rel A_rel_dec x tl else filter_rel A_rel_dec x tl
  end.

Definition map2fst {A B : Type} (a : A) := map (fun (b : B) => (a, b)).

Definition map2snd {A B : Type} (b : B) := map (fun (a : A) => (a, b)).

Section Update2.
  Variables A B : Type.

  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.
  
  Lemma update2_diff1 :
    forall (sigma : A -> A -> B) x y v x' y',
      x <> x' ->
      update2 A_eq_dec sigma x y v x' y' = sigma x' y'.
  Proof using.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq B (if sumbool_and (@eq A x x') (not (@eq A x x')) (@eq A y y') (not (@eq A y y')) (A_eq_dec x x') (A_eq_dec y y') then v else sigma x' y') v *)
    break_if; intuition congruence.
  Qed.

  Lemma update2_diff2 :
    forall (sigma : A -> A -> B) x y v x' y',
      y <> y' ->
      update2 A_eq_dec sigma x y v x' y' = sigma x' y'.
  Proof using.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq B (if sumbool_and (@eq A x x') (not (@eq A x x')) (@eq A y y') (not (@eq A y y')) (A_eq_dec x x') (A_eq_dec y y') then v else sigma x' y') v *)
    break_if; intuition congruence.
  Qed.

  Lemma update2_diff_prod :
    forall (sigma : A -> A -> B) x y v x' y',
      (x, y) <> (x', y') ->
      update2 A_eq_dec sigma x y v x' y' = sigma x' y'.
  Proof using.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq B (if sumbool_and (@eq A x x') (not (@eq A x x')) (@eq A y y') (not (@eq A y y')) (A_eq_dec x x') (A_eq_dec y y') then v else sigma x' y') v *)
    break_if; intuition congruence.
  Qed.
  
  Lemma update2_nop :
    forall (sigma : A -> A -> B) x y x' y',
      update2 A_eq_dec sigma x y (sigma x y) x' y' = sigma x' y'.
  Proof using.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros. break_if; intuition congruence.
  Qed.

  Lemma update2_eq :
    forall (sigma : A -> A -> B) x y x' y' v,
      x = x' ->
      y = y' ->
      update2 A_eq_dec sigma x y v x' y' = v.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros. subst.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: @eq B (if sumbool_and (@eq A x x') (not (@eq A x x')) (@eq A y y') (not (@eq A y y')) (A_eq_dec x x') (A_eq_dec y y') then v else sigma x' y') v *)
    break_if; intuition congruence.
  Qed.

  Lemma update2_eq_prod :
    forall (sigma : A -> A -> B) x y x' y' v,
      (x, y) = (x', y') ->
      update2 A_eq_dec sigma x y v x' y' = v.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros. subst.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: @eq B (if sumbool_and (@eq A x x') (not (@eq A x x')) (@eq A y y') (not (@eq A y y')) (A_eq_dec x x') (A_eq_dec y y') then v else sigma x' y') v *)
    break_if; intuition congruence.
  Qed.
  
  Lemma update2_same :
    forall (sigma : A -> A -> B) x y v,
      update2 A_eq_dec sigma x y v x y = v.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq B (@update2 A B A_eq_dec sigma x y v x y) v *)
    rewrite update2_eq; auto.
  Qed.

  Lemma update2_nop_ext :
    forall (sigma : A -> A -> B) x y,
      update2 A_eq_dec sigma x y (sigma x y) = sigma.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (forall (_ : A) (_ : A), B) (@update2 A B A_eq_dec (@update2 A B A_eq_dec sigma x y st) x y st') (@update2 A B A_eq_dec sigma x y st') *)
    do 2 (apply functional_extensionality; intros).
(* Goal: @eq B (@update2 A B A_eq_dec sigma x y (sigma x y) x0 x1) (sigma x0 x1) *)
    apply update2_nop.
  Qed.

  Lemma update2_nop_ext' :
    forall (sigma : A -> A -> B) x y v,
      sigma x y = v ->
      update2 A_eq_dec sigma x y v = sigma.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: @eq (forall (_ : A) (_ : A), B) (@update2 A B A_eq_dec sigma x y (sigma x y)) sigma *)
    apply update2_nop_ext.
  Qed.

  Lemma update2_overwrite :
    forall (sigma : A -> A -> B) x y st st',
      update2 A_eq_dec (update2 A_eq_dec sigma x y st) x y st' = update2 A_eq_dec sigma x y st'.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (forall (_ : A) (_ : A), B) (@update2 A B A_eq_dec (@update2 A B A_eq_dec sigma x y st) x y st') (@update2 A B A_eq_dec sigma x y st') *)
    do 2 (apply functional_extensionality; intros).
    destruct (A_eq_dec x x0);
      destruct (A_eq_dec y x1).
(* Goal: @eq B (@update2 A B A_eq_dec sigma x y v x y) v *)
    - repeat rewrite update2_eq; auto.
    - repeat rewrite update2_diff2; auto.
    - repeat rewrite update2_diff1; auto.
    - repeat rewrite update2_diff1; auto.
  Qed.

End Update2.


Lemma update2_fun_comm :
  forall A B C A_eq_dec (f : B -> C) (st : A -> A -> B) x y v x' y',
    f (update2 A_eq_dec st x y v x' y') = update2 A_eq_dec (fun x y => f (st x y)) x y (f v) x' y'.
Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
  intros.
  destruct (prod_eq_dec A_eq_dec A_eq_dec (x, y) (x', y')); subst;
    repeat first [rewrite update2_diff_prod by congruence |
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
                  rewrite update2_eq_prod  by auto ]; auto.
Qed.

Ltac update2_destruct_goal :=
  match goal with
  | [ |- context [ update2 ?eq_dec _ ?x ?y _ ?x' ?y' ] ] =>
    destruct (prod_eq_dec eq_dec eq_dec (x, y) (x', y'))
  end.

Ltac update2_destruct_hyp :=
  match goal with
  | [ _ : context [ update2 ?eq_dec _ ?x ?y _ ?x' ?y' ] |- _ ] =>
    destruct (prod_eq_dec eq_dec eq_dec (x, y) (x', y'))
  end.

Ltac update2_destruct := update2_destruct_goal || update2_destruct_hyp.

Ltac rewrite_update2' H :=
  first [rewrite update2_diff_prod in H by congruence |
         rewrite update2_eq_prod in H by auto ].

Ltac rewrite_update2 :=
  repeat match goal with
           | [ H : context [ update2 _ _ _ _ _ _ _ ] |- _ ] =>
             rewrite_update2' H; repeat rewrite_update2' H
           | [ |- _ ] => repeat (try rewrite update2_diff_prod by congruence;
                                 try rewrite update2_eq_prod by auto)
         end.

Ltac destruct_update2 :=
  repeat (update2_destruct; subst; rewrite_update2).

Ltac destruct_update2_hyp :=
  repeat ((update2_destruct_hyp || update2_destruct_goal); subst; rewrite_update2).

Ltac update2_destruct_simplify :=
  update2_destruct; subst; rewrite_update2; simpl in *.

Ltac update2_destruct_simplify_hyp :=
  update2_destruct_hyp || update2_destruct_goal; subst; rewrite_update2; simpl in *.

Ltac update2_destruct_max_simplify :=
  update2_destruct; subst_max; rewrite_update2; simpl in *.

Section Update2Rel.
  Variables A B : Type.
  Variable R : relation A.

  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.
  Hypothesis R_dec : forall x y : A, {R x y} + {~ R x y}.

  Lemma filter_rel_related :
    forall n n' ns,
      In n' (filter_rel R_dec n ns) ->
      In n' ns /\ R n n'.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @In A n' (@filter_rel A R R_dec n ns) *)
    induction ns; simpl in *; [ intuition | idtac ].
(* Goal: and (R h n) (or (@eq A a n) (@In A n ns)) *)
    break_if; simpl in *.
    - break_or_hyp; auto.
(* Goal: @NoDup (prod A B) (@map2snd A B m (@filter_rel A R R_dec h (@cons A a ns))) *)
      concludes.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
      break_and.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      auto.
    - concludes.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
      break_and.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      auto.
  Qed.

  Lemma related_filter_rel : 
    forall n n' ns,
      In n' ns -> 
      R n n' ->
      In n' (filter_rel R_dec n ns).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @In A n' (@filter_rel A R R_dec n ns) *)
    induction ns; simpl in *; [ intuition | idtac ].
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (if sumbool_and (@eq A h' h') (not (@eq A h' h')) (@eq A h h) (not (@eq A h h)) (A_eq_dec h' h') (A_eq_dec h h) then @app B (f' h' h) (@cons B m (@nil B)) else f' h' h) *)
    break_if.
    - break_or_hyp.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      * left; auto.
(* Goal: @NoDup (prod A B) (@map2snd A B m (@filter_rel A R R_dec h (@cons A a ns))) *)
      * concludes.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        right; auto.
    - break_or_hyp.
      * intuition.
(* Goal: @NoDup (prod A B) (@map2snd A B m (@filter_rel A R R_dec h (@cons A a ns))) *)
      * concludes.
(* Goal: @Permutation A l (@app A x x0) *)
        assumption.
  Qed.

  Lemma not_in_not_in_filter_rel :
    forall ns n h,
      ~ In n ns ->
      ~ In n (filter_rel R_dec h ns).
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg n h) (f n h) *)
    assert (H_neq: a <> n).
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: False *)
(* Goal: not (@In A n (@filter_rel A R R_dec h (@cons A a ns))) *)
    auto with datatypes.
(* Goal: not (@In A n (@filter_rel A R R_dec h (@cons A a ns))) *)
    assert (H_not_in: ~ In n ns).
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: False *)
    break_or_hyp; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    intuition eauto.
  Qed.

  Lemma NoDup_filter_rel:
    forall h ns,
      NoDup ns ->
      NoDup (filter_rel R_dec h ns).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    invc_NoDup.
(* Goal: @NoDup (prod A B) (@map2snd A B m (@filter_rel A R R_dec h (@cons A a ns))) *)
    concludes.
    simpl in *.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    apply NoDup_cons; auto.
(* Goal: not (@In A n (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) *)
    apply not_in_not_in_filter_rel.
(* Goal: @Permutation A l (@app A x x0) *)
    assumption.
  Qed.

  Lemma filter_rel_self_eq {irreflexive_R : Irreflexive R} :
    forall ns0 ns1 h,
      filter_rel R_dec h (ns0 ++ h :: ns1) = filter_rel R_dec h (ns0 ++ ns1).
  Proof using.
    induction ns0; intros; simpl in *.
    - break_if; auto.
(* Goal: @eq (list A) (@cons A h (@filter_rel A R R_dec h ns1)) (@filter_rel A R R_dec h ns1) *)
      find_apply_lem_hyp irreflexive_R.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
    - break_if; auto.
(* Goal: @eq (list A) (@cons A a (@filter_rel A R R_dec h (@app A ns0 (@cons A h ns1)))) (@cons A a (@filter_rel A R R_dec h (@app A ns0 ns1))) *)
      find_higher_order_rewrite.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
  Qed.

  Lemma collate_f_eq :
    forall (f : A -> A -> list B) g h n n' l,
      f n n' = g n n' ->
      collate A_eq_dec h f l n n' = collate A_eq_dec h g l n n'.
  Proof using.
(* Goal: forall (f g : forall (_ : A) (_ : A), list B) (h n n' : A) (l : list (prod A B)) (_ : @eq (list B) (f n n') (g n n')), @eq (list B) (@collate A B A_eq_dec h f l n n') (@collate A B A_eq_dec h g l n n') *)
    intros f g h n n' l.
(* Goal: forall _ : @eq (list B) (f n n') (g n n'), @eq (list B) (@collate A B A_eq_dec h f l n n') (@collate A B A_eq_dec h g l n n') *)
    generalize f g; clear f g.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l; auto.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
    simpl in *.
(* Goal: @eq (list B) ((let (to, m) := a in @collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@collate A B A_eq_dec h f l1) h to (@app B (@collate A B A_eq_dec h f l1 h to) (@cons B m (@nil B)))) l2) h h') (@collate A B A_eq_dec h f l1 h h') *)
    break_let.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
    destruct a.
(* Goal: False *)
    find_injection.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A x (@cons A a x0)) f h m) *)
    set (f' := update2 _ _ _ _ _).
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns f' h mg n n') (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec g a h (@app B (g a h) (@cons B mg (@nil B)))) h mg n n') *)
    set (g' := update2 _ _ _ _ _).
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite (IHl f' g'); auto.
(* Goal: @eq (list B) (f' n n') (g' n n') *)
    unfold f', g', update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
    break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: @In B x (f a b) *)
    find_rewrite.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
  Qed.

  Lemma collate_in_in :
    forall l h n n' (f : A -> A -> list B) a,
      In a (f n' n) ->
      In a ((collate A_eq_dec h f l) n' n).
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l; intros; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
    destruct a.
(* Goal: @eq (option B) (@hd_error B (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a (@app B (f h a) (@cons B b (@nil B)))) l n' n)) (@Some B a0) *)
    apply IHl.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
    break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: @In A h' (@app A l1 l2) *)
    apply in_or_app.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    left.
(* Goal: @Permutation A l (@app A x x0) *)
    assumption.
  Qed.

  Lemma collate_head_head :
    forall l h n n' (f : A -> A -> list B) a,
      head (f n' n) = Some a ->
      head ((collate A_eq_dec h f l) n' n) = Some a.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l; intros; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
    destruct a.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: @eq (option B) (@hd_error B (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a (@app B (f h a) (@cons B b (@nil B)))) l n' n)) (@Some B a0) *)
    apply IHl.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    destruct (f n' n); auto.
(* Goal: @eq (option B) (@hd_error B (@app B (@nil B) (@cons B b (@nil B)))) (@Some B a0) *)
    find_apply_lem_hyp hd_error_some_nil.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
  Qed.

  Lemma collate_neq :
    forall h n n' ns (f : A -> A -> list B),
      h <> n ->
      collate A_eq_dec h f ns n n' = f n n'.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
    destruct a.
    simpl in *.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg n h) (f n h) *)
    rewrite IHns.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
  Qed.

  Lemma collate_not_in_eq :
    forall h' h (f : A -> A -> list B) l,
      ~ In h (map fst l) ->
      collate A_eq_dec h' f l h' h = f h' h.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l; intros; auto.
    simpl in *.
(* Goal: @eq (list B) ((let (to, m) := a in @collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@collate A B A_eq_dec h f l1) h to (@app B (@collate A B A_eq_dec h f l1 h to) (@cons B m (@nil B)))) l2) h h') (@collate A B A_eq_dec h f l1 h h') *)
    break_let.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
    destruct a.
(* Goal: False *)
    find_injection.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    rewrite IHl; unfold update2.
    - break_if.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      * break_and; subst.
        simpl in *.
(* Goal: False *)
        contradict H.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        trivial.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      * intros.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        trivial.
    - intro.
(* Goal: False *)
      contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
      right.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
  Qed.

  Lemma collate_app :
    forall h' l1 l2 (f : A -> A -> list B),
      collate A_eq_dec h' f (l1 ++ l2) = collate A_eq_dec h' (collate A_eq_dec h' f l1) l2.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l1; intros; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: @eq (list B) ((let (to, m) := a in @collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@collate A B A_eq_dec h f l1) h to (@app B (@collate A B A_eq_dec h f l1 h to) (@cons B m (@nil B)))) l2) h h') (@collate A B A_eq_dec h f l1 h h') *)
    break_let.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
    destruct a.
(* Goal: False *)
    find_injection.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a0 (@app B (f h a0) (@cons B b (@nil B)))) l1) l2 h h') (@collate A B A_eq_dec h f l2 h h') *)
    rewrite IHl1.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
  Qed.

  Lemma collate_neq_update2 :
    forall h h' n (f : A -> A -> list B) l ms,
      n <> h' ->
      collate A_eq_dec h (update2 A_eq_dec f h n ms) l h h' = collate A_eq_dec h f l h h'.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
    assert (H_eq: update2 A_eq_dec f h n ms h h' =  f h h').
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h n ms) l h h') (@collate A B A_eq_dec h f l h h') *)
    rewrite (collate_f_eq _ _ _ _ _ _ H_eq).
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
  Qed.

  Lemma collate_not_in :
    forall h h' l1 l2 (f : A -> A -> list B),
      ~ In h' (map fst l1) ->
      collate A_eq_dec h f (l1 ++ l2) h h' = collate A_eq_dec h f l2 h h'.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@collate A B A_eq_dec h' f l1) l2 h' to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' to) *)
    rewrite collate_app.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l1; intros; simpl in *; auto.
(* Goal: @eq (list B) ((let (to, m) := a in @collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@collate A B A_eq_dec h f l1) h to (@app B (@collate A B A_eq_dec h f l1 h to) (@cons B m (@nil B)))) l2) h h') (@collate A B A_eq_dec h f l1 h h') *)
    break_let.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a0 (@app B (f h a0) (@cons B b (@nil B)))) l1) l2 h h') (@collate A B A_eq_dec h f l2 h h') *)
    rewrite IHl1.
    - destruct a.
(* Goal: False *)
      find_injection.
      simpl in *.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a0 (@app B (f h a0) (@cons B b (@nil B)))) l2 h h') (@collate A B A_eq_dec h f l2 h h') *)
      assert (H_neq: a0 <> h').
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: False *)
      contradict H.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      rewrite collate_neq_update2; trivial.
    - intro.
(* Goal: False *)
      contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
      right.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
  Qed.

  Lemma collate_not_in_rest :
    forall h h' l1 l2 (f : A -> A -> list B),
      ~ In h' (map fst l2) ->
      collate A_eq_dec h f (l1 ++ l2) h h' = collate A_eq_dec h f l1 h h'.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@collate A B A_eq_dec h' f l1) l2 h' to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' to) *)
    rewrite collate_app.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l2; intros; simpl in *; auto.
(* Goal: @eq (list B) ((let (to, m) := a in @collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@collate A B A_eq_dec h f l1) h to (@app B (@collate A B A_eq_dec h f l1 h to) (@cons B m (@nil B)))) l2) h h') (@collate A B A_eq_dec h f l1 h h') *)
    break_let.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst_max.
    simpl in *.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    assert (H_neq: a0 <> h'); auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite collate_neq_update2; auto.
  Qed.

  Lemma collate_not_in_mid :
    forall h h' l1 l2 (f : A -> A -> list B) m,
      ~ In h (map fst (l1 ++ l2)) ->
      collate A_eq_dec h' (update2 A_eq_dec f h' h (f h' h ++ [m])) (l1 ++ l2) = collate A_eq_dec h' f (l1 ++ (h, m) :: l2).
  Proof using.
(* Goal: forall (h h' : A) (l1 l2 : list A) (f : forall (_ : A) (_ : A), list B) (m : B) (_ : not (@In A h' (@app A l1 l2))), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@app A l1 l2) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A l1 (@cons A h' l2)) f h m) *)
    intros h h' l1 l2 f m H_in.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@app A l1 l2) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A l1 (@cons A h' l2)) f h m) *)
    apply functional_extensionality; intro from.
(* Goal: @eq (forall _ : A, list B) (@collate_ls A B A_eq_dec (@app A l1 l2) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) h m from) (@collate_ls A B A_eq_dec (@app A l1 (@cons A h' l2)) f h m from) *)
    apply functional_extensionality; intro to.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) (@app (prod A B) l1 l2) from to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) from to) *)
    case (A_eq_dec h' from); intro H_dec.
    - rewrite <- H_dec.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) (@app (prod A B) l1 l2) h' to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' to) *)
      case (A_eq_dec h to); intro H_dec'.
      * rewrite <- H_dec'.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) (@app (prod A B) l1 l2) h' h) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' h) *)
        rewrite collate_not_in.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      + subst.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        rewrite collate_not_in; auto.
(* Goal: not (@In A a (@app A x x0)) *)
        intro.
(* Goal: False *)
        contradict H_in.
(* Goal: @In A h (@map (prod A B) A (@fst A B) (@app (prod A B) l1 l2)) *)
        rewrite map_app.
(* Goal: @In A h' (@app A l1 l2) *)
        apply in_or_app.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        left.
(* Goal: @Permutation A l (@app A x x0) *)
        assumption.
(* Goal: not (@In A a (@app A x x0)) *)
      + intro.
(* Goal: False *)
        contradict H_in.
(* Goal: @In A h (@map (prod A B) A (@fst A B) (@app (prod A B) l1 l2)) *)
        rewrite map_app.
(* Goal: @In A h' (@app A l1 l2) *)
        apply in_or_app.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        left.
(* Goal: @Permutation A l (@app A x x0) *)
        assumption.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        * rewrite collate_neq_update2; auto.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@collate A B A_eq_dec h' f l1) l2 h' to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' to) *)
          rewrite collate_app.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@collate A B A_eq_dec h' f l1) l2 h' to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' to) *)
          rewrite collate_app.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
          simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
          rewrite collate_neq_update2; auto.
    - rewrite collate_neq; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_neq; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
  Qed.

  Lemma NoDup_Permutation_collate_eq :
    forall h (f : A -> A -> list B) l l',
      NoDup (map fst l) ->
      Permutation l l' ->
      collate A_eq_dec h f l = collate A_eq_dec h f l'.
  Proof using.
(* Goal: forall (h : A) (f : forall (_ : A) (_ : A), list B) (l l' : list (prod A B)) (_ : @NoDup A (@map (prod A B) A (@fst A B) l)) (_ : @Permutation (prod A B) l l'), @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f l) (@collate A B A_eq_dec h f l') *)
    intros h f l.
(* Goal: forall (l' : list (prod A B)) (_ : @NoDup A (@map (prod A B) A (@fst A B) l)) (_ : @Permutation (prod A B) l l'), @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f l) (@collate A B A_eq_dec h f l') *)
    revert h f.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A l) (_ : @Permutation A l l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    induction l.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - intros.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      find_apply_lem_hyp Permutation_nil.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      subst.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - intros.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h f (@cons (prod A B) a l)) (@collate A B A_eq_dec h f l') *)
      destruct a.
      simpl in *.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      invc_NoDup.  
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a (@app B (f h a) (@cons B b (@nil B)))) l) (@collate A B A_eq_dec h f l') *)
      assert (H_in': In (a, b) ((a, b) :: l)). 
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a (@app B (f h a) (@cons B b (@nil B)))) l) (@collate A B A_eq_dec h f l') *)
      pose proof (Permutation_in _ H0 H_in') as H_pm'.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a (@app B (f h a) (@cons B b (@nil B)))) l) (@collate A B A_eq_dec h f l') *)
      apply in_split in H_pm'.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      break_exists; subst.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A x (@cons A a x0)) f h m) *)
      find_apply_lem_hyp Permutation_cons_app_inv.
      pose proof (IHl h (update2 A_eq_dec f h a (f h a ++ [b])) _ H4 H0) as IHl'.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h a (@app B (f h a) (@cons B b (@nil B)))) l) (@collate A B A_eq_dec h f (@app (prod A B) x (@cons (prod A B) (@pair A B a b) x0))) *)
      rewrite IHl'.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_not_in_mid; auto.
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
      assert (H_pm': Permutation (map (fun nm : A * B => fst nm) l) (map (fun nm : A * B => fst nm) (x ++ x0))).
(* Goal: @Permutation A (@map (prod A B) A (fun nm : prod A B => @fst A B nm) l) (@map (prod A B) A (fun nm : prod A B => @fst A B nm) (@app (prod A B) x x0)) *)
(* Goal: False *)
      apply Permutation_map_fst.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: False *)
      contradict H3.
(* Goal: @In A a l *)
      revert H.
(* Goal: forall _ : @In A a (@app A x x0), @In A a l *)
      apply Permutation_in.
(* Goal: @Permutation A (@app A x x0) l *)
      apply Permutation_sym.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
  Qed.

  Lemma collate_map2snd_not_related :
    forall m n h ns (f : A -> A -> list B),
      ~ R h n ->
      collate A_eq_dec h f (map2snd m (filter_rel R_dec h ns)) h n = f h n.
  Proof using.
(* Goal: forall (m : B) (n h : A) (ns : list A) (f : forall (_ : A) (_ : A), list B) (_ : not (R h n)), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h ns)) h n) (f h n) *)
    intros m n h ns f H_adj.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; simpl; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg n h) (f n h) *)
    rewrite IHns.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
  Qed.

  Lemma collate_map2snd_in_neq_in_before :
    forall from (f : A -> A -> list B) m dsts a b x,
      In x (collate A_eq_dec from f (map2snd m dsts) a b) ->
      x <> m ->
      In x (f a b).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: or (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (@app B (f a b) l)))) *)
    generalize dependent f.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (_ : @In B x (@collate A B A_eq_dec from f (@map2snd A B m dsts) a b)), @In B x (f a b) *)
    induction dsts.
    - auto.
    - simpl; intros f H_coll.
(* Goal: @In B x (f a b) *)
      eapply IHdsts in H_coll.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      destruct (A_eq_dec from a), (A_eq_dec a0 b); subst.
      + rewrite update2_same in *.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
        find_eapply_lem_hyp in_app_or; break_or_hyp.
        * assumption.
        * exfalso;
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
          find_eapply_lem_hyp in_inv; break_or_hyp; exfalso; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      + rewrite update2_diff2 in *; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      + rewrite update2_diff1 in *; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      + rewrite update2_diff1 in *; auto.
  Qed.

  Lemma collate_map2snd_not_in :
    forall m n h ns (f : A -> A -> list B),
      ~ In n ns ->
      collate A_eq_dec h f (map2snd m (filter_rel R_dec h ns)) h n = f h n.
  Proof using.
(* Goal: forall (m : B) (n h : A) (ns : list A) (f : forall (_ : A) (_ : A), list B) (_ : not (@In A n ns)), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h ns)) h n) (f h n) *)
    intros m n h ns f.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
    simpl in *.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    break_if; simpl.
    - rewrite IHns.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      * unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
        break_and; subst.
(* Goal: False *)
        contradict H.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        trivial.
      * intro.
(* Goal: False *)
        contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
        right.
(* Goal: @Permutation A l (@app A x x0) *)
        assumption.
    - rewrite IHns; auto.
  Qed.

  Lemma collate_map2snd_not_in_remove_all :
    forall m n h ns (f : A -> A -> list B) ns',
      ~ In n ns ->
      collate A_eq_dec h f (map2snd m (filter_rel R_dec h (remove_all A_eq_dec ns' ns))) h n = f h n.
  Proof using.
(* Goal: forall (m : B) (n h : A) (ns : list A) (f : forall (_ : A) (_ : A), list B) (ns' : list A) (_ : not (@In A n ns)), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) h n) (f h n) *)
    intros m n h ns f ns' H_in.
(* Goal: @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) h n) (f h n) *)
    apply collate_map2snd_not_in.
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: False *)
    find_apply_lem_hyp in_remove_all_was_in.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
  Qed.

  Lemma collate_map2snd_not_in_related :
    forall m n h ns (f : A -> A -> list B) ns',
      ~ In n ns' ->
      R h n ->
      In n ns ->
      NoDup ns ->
      collate A_eq_dec h f (map2snd m (filter_rel R_dec h (remove_all A_eq_dec ns' ns))) h n = f h n ++ [m].
  Proof using.
(* Goal: forall (m : B) (n h : A) (ns : list A) (f : forall (_ : A) (_ : A), list B) (ns' : list A) (_ : not (@In A n ns')) (_ : R h n) (_ : @In A n ns) (_ : @NoDup A ns), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) h n) (@app B (f h n) (@cons B m (@nil B))) *)
    intros m n h ns f ns' H_in H_adj.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (_ : @In A n ns) (_ : @NoDup A ns), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) h n) (@app B (f h n) (@cons B m (@nil B))) *)
    induction ns; intros; [ contradict H | idtac ].
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    invc_NoDup.
    simpl in *.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
    break_or_hyp.
    - pose proof (remove_all_cons A_eq_dec ns' n ns) as H_ra.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      break_or_hyp; break_and; intuition.
(* Goal: @In B x (f a b) *)
      find_rewrite.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      simpl.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      break_if; intuition.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_map2snd_not_in_remove_all; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
    - assert (H_neq: a <> n).
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.  
(* Goal: @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' (@cons A a ns)))) h n) (f h n) *)
      pose proof (remove_all_cons A_eq_dec ns' a ns) as H_ra.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
      break_or_hyp; break_and. 
      * find_rewrite.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        rewrite IHns; auto.
      * find_rewrite.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
        simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
        simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        rewrite IHns; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
        unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
        break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
        subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
        intuition.
  Qed.

  Lemma collate_map2snd_in :
    forall m n h ns (f : A -> A -> list B) ns',
      In n ns' ->
      collate A_eq_dec h f (map2snd m (filter_rel R_dec h (remove_all A_eq_dec ns' ns))) h n = f h n.
  Proof using.
(* Goal: forall (m : B) (n h : A) (ns : list A) (f : forall (_ : A) (_ : A), list B) (ns' : list A) (_ : @In A n ns'), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B m (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) h n) (f h n) *)
    intros m n h ns f ns'.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    induction ns; intros.
    - rewrite remove_all_nil.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
    - pose proof (remove_all_cons A_eq_dec ns' a ns) as H_ra.
(* Goal: @In B x (f a b) *)
      break_or_hyp; break_and; find_rewrite.
      * rewrite IHns; trivial.
      * simpl.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (if sumbool_and (@eq A h' h') (not (@eq A h' h')) (@eq A h h) (not (@eq A h h)) (A_eq_dec h' h') (A_eq_dec h h) then @app B (f' h' h) (@cons B m (@nil B)) else f' h' h) *)
        break_if.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      + simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        rewrite IHns; simpl; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
        unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
        break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
        intuition.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      + rewrite IHns; trivial.
  Qed.

  Lemma collate_map2snd_related_not_in :
    forall a n h ns (f : A -> A -> list B),
      R h n ->
      ~ In n ns ->
      collate A_eq_dec h f (map2snd a (filter_rel R_dec h (n :: ns))) h n = f h n ++ [a].
  Proof using.
(* Goal: forall (a : B) (n h : A) (ns : list A) (f : forall (_ : A) (_ : A), list B) (_ : R h n) (_ : not (@In A n ns)), @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B a (@filter_rel A R R_dec h (@cons A n ns))) h n) (@app B (f h n) (@cons B a (@nil B))) *)
    intros a n h ns f H_adj H_in.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    break_if; intuition.
(* Goal: @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B a (@cons A n (@filter_rel A R R_dec h ns))) h n) (@app B (f h n) (@cons B a (@nil B))) *)
    clear r.
(* Goal: @eq (list B) (@collate A B A_eq_dec h f (@map2snd A B a (@cons A n (@filter_rel A R R_dec h ns))) h n) (@app B (f h n) (@cons B a (@nil B))) *)
    revert f n h H_in H_adj.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    induction ns; intros; simpl.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    - unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
    - assert (H_in': ~ In n ns).
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: False *)
      contradict H_in.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
      right.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec f h n (@app B (f h n) (@cons B a (@nil B)))) (@map2snd A B a (if R_dec h a0 then @cons A a0 (@filter_rel A R R_dec h ns) else @filter_rel A R R_dec h ns)) h n) (@app B (f h n) (@cons B a (@nil B))) *)
      assert (H_neq: n <> a0). 
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      subst.
(* Goal: False *)
      contradict H_in.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
      simpl in *.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (if sumbool_and (@eq A h' h') (not (@eq A h' h')) (@eq A h h) (not (@eq A h h)) (A_eq_dec h' h') (A_eq_dec h h) then @app B (f' h' h) (@cons B m (@nil B)) else f' h' h) *)
      break_if.
      * simpl.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@update2 A (list B) A_eq_dec f h n (@app B (f h n) (@cons B a (@nil B)))) h a0 (@app B (@update2 A (list B) A_eq_dec f h n (@app B (f h n) (@cons B a (@nil B))) h a0) (@cons B a (@nil B)))) (@map2snd A B a (@filter_rel A R R_dec h ns)) h n) (@app B (f h n) (@cons B a (@nil B))) *)
        unfold update2 at 3.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; intuition eauto.
(* Goal: @eq (list B) (@collate A B A_eq_dec h (@update2 A (list B) A_eq_dec (@update2 A (list B) A_eq_dec f h n (@app B (f h n) (@cons B a (@nil B)))) h a0 (@app B (f h a0) (@cons B a (@nil B)))) (@map2snd A B a (@filter_rel A R R_dec h ns)) h n) (@app B (f h n) (@cons B a (@nil B))) *)
        pose proof (IHns f) as IH'.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        rewrite collate_map2snd_not_in; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
        unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; intuition eauto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
        intuition.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      * rewrite IHns; auto.
  Qed.

  Lemma in_collate_in :
    forall ns n h (f : A -> A -> list B) a,
      ~ In n ns ->
      In a (collate A_eq_dec h f (map2snd a (filter_rel R_dec h ns)) h n) ->
      In a (f h n).
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
(* Goal: @In B a0 (f h n) *)
    assert (H_in': ~ In n ns).
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: False *)
    contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
    right.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
(* Goal: @In B a0 (f h n) *)
    assert (H_neq: n <> a). 
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: False *)
    contradict H.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
    simpl in *.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
    simpl in *.
    assert (H_eq_f: update2 A_eq_dec f h a (f h a ++ [a0]) h n = f h n).
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
(* Goal: @In B a0 (f h n) *)
    rewrite (collate_f_eq _ _ _ _ _ _ H_eq_f) in H0.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    apply IHns; auto.
  Qed.

  Lemma not_in_map2snd :
    forall n h (m : B) ns,
      ~ In n ns ->
      ~ In (n, m) (map2snd m (filter_rel R_dec h ns)).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
    simpl in *.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (if sumbool_and (@eq A h' h') (not (@eq A h' h')) (@eq A h h) (not (@eq A h h)) (A_eq_dec h' h') (A_eq_dec h h) then @app B (f' h' h) (@cons B m (@nil B)) else f' h' h) *)
    break_if.
    - simpl.
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
      break_or_hyp.
      * find_injection.
(* Goal: False *)
        contradict H.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        trivial.
      * contradict H1.
(* Goal: @eq B (@snd A B nm) m *)
        apply IHns.
(* Goal: not (@In A a (@app A x x0)) *)
        intro.
(* Goal: False *)
        contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
        right.
(* Goal: @Permutation A l (@app A x x0) *)
        assumption.
    - apply IHns.
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: False *)
      contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
      right.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
  Qed.

  Lemma NoDup_map2snd :
    forall h (m : B) ns,
      NoDup ns ->
      NoDup (map2snd m (filter_rel R_dec h ns)).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (_ : @In B x (f a b)), @In B x (@collate_ls A B A_eq_dec ns f to m a b) *)
    induction ns.
    - apply NoDup_nil.
    - invc_NoDup.
(* Goal: @NoDup (prod A B) (@map2snd A B m (@filter_rel A R R_dec h (@cons A a ns))) *)
      concludes.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      apply NoDup_cons; auto.
(* Goal: not (@In (prod A B) (@pair A B a m) (@map2snd A B m (@filter_rel A R R_dec h ns))) *)
      apply not_in_map2snd.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
  Qed.

  Lemma in_map2snd_snd :
    forall h (m : B) ns nm,
      In nm (map2snd m (filter_rel R_dec h ns)) ->
      snd nm = m.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
    induction ns; intros; simpl in *; intuition.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (if sumbool_and (@eq A h' h') (not (@eq A h' h')) (@eq A h h) (not (@eq A h h)) (A_eq_dec h' h') (A_eq_dec h h) then @app B (f' h' h) (@cons B m (@nil B)) else f' h' h) *)
    break_if.
    - simpl in *.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_or_hyp; intuition eauto.
    - apply IHns.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
  Qed.

  Lemma in_map2snd_related_in :
    forall (m : B) ns n h,
      In (n, m) (map2snd m (filter_rel R_dec h ns)) ->
      R h n /\ In n ns.
  Proof using.
(* Goal: forall (m : B) (ns : list A) (n h : A) (_ : @In (prod A B) (@pair A B n m) (@map2snd A B m (@filter_rel A R R_dec h ns))), and (R h n) (@In A n ns) *)
    intros m.
    induction ns; intros; simpl in *; [ intuition | idtac ].
(* Goal: and (R h n) (or (@eq A a n) (@In A n ns)) *)
    break_if; simpl in *.
    - break_or_hyp.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      * find_injection; auto.
      * find_apply_hyp_hyp.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
        break_and.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        auto.
    - find_apply_hyp_hyp.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
      break_and.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      auto.
  Qed.

  Lemma collate_ls_not_in :
    forall ns (f : A -> A -> list B) h mg from to,
      ~ In from ns ->
      collate_ls A_eq_dec ns f h mg from to = f from to.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
    assert (H_neq: a <> from).
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: False *)
    contradict H.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a ns) f h mg from to) (f from to) *)
    assert (H_in': ~ In from ns).
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: False *)
    contradict H.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
    right.
(* Goal: @Permutation A l (@app A x x0) *)
    assumption.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
    simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite IHns; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition. 
  Qed.

  Lemma collate_ls_in_in :
    forall ns (f : A -> A -> list B) to m x a b,
      In x (f a b) ->
      In x (collate_ls A_eq_dec ns f to m a b).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: or (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (@app B (f a b) l)))) *)
    generalize dependent f.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (_ : @In B x (f a b)), @In B x (@collate_ls A B A_eq_dec ns f to m a b) *)
    induction ns.
    - auto.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      eapply IHns; eauto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      destruct (A_eq_dec a a0), (A_eq_dec to b); subst.
      + rewrite update2_eq; auto using in_or_app.
      + rewrite update2_diff2; auto using in_or_app.
      + rewrite update2_diff1; auto using in_or_app.
      + rewrite update2_diff1; auto using in_or_app.
  Qed.

  Lemma collate_ls_neq_to : 
    forall ns (f : A -> A -> list B) h mg from to,
      h <> to ->
      collate_ls A_eq_dec ns f h mg from to = f from to.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; auto.
    simpl in *.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite IHns; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
  Qed.

  Lemma collate_ls_NoDup_in :
    forall ns (f : A -> A -> list B) h mg from,
      NoDup ns ->
      In from ns ->
      collate_ls A_eq_dec ns f h mg from h = f from h ++ [mg].
  Proof using.
    induction ns; intros; simpl in *; [ intuition | idtac ].
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    invc_NoDup.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
    break_or_hyp.
    - rewrite collate_ls_not_in; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      break_or_hyp; intuition.
    - assert (H_neq: a <> from).
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: @In B x (f a b) *)
      find_rewrite.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite IHns; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
  Qed.

  Lemma collate_ls_live_related : 
    forall ns (f : A -> A -> list B) ns' h mg from,
      ~ In from ns' ->
      R h from ->
      In from ns ->
      NoDup ns ->
      collate_ls A_eq_dec (filter_rel R_dec h (remove_all A_eq_dec ns' ns)) f h mg from h = f from h ++ [mg].
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite collate_ls_NoDup_in; auto.
    - apply NoDup_filter_rel.
(* Goal: @NoDup A (@remove_all A A_eq_dec ns' ns) *)
      apply NoDup_remove_all.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
    - apply related_filter_rel.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      apply in_remove_all_preserve; auto.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
  Qed.

  Lemma collate_ls_f_eq :
    forall ns (f : A -> A -> list B) g h mg n n',
      f n n' = g n n' ->
      collate_ls A_eq_dec ns f h mg n n' = collate_ls A_eq_dec ns g h mg n n'.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; simpl in *; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A x (@cons A a x0)) f h m) *)
    set (f' := update2 _ _ _ _ _).
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns f' h mg n n') (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec g a h (@app B (g a h) (@cons B mg (@nil B)))) h mg n n') *)
    set (g' := update2 _ _ _ _ _).
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite (IHns f' g'); auto.
(* Goal: @eq (list B) (f' n n') (g' n n') *)
    unfold f', g', update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
    break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: @In B x (f a b) *)
    find_rewrite.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
  Qed.

  Lemma collate_ls_neq_update2 : 
    forall ns (f : A -> A -> list B) n h h' ms mg,
      n <> h' ->
      collate_ls A_eq_dec ns (update2 A_eq_dec f n h ms) h mg h' h = collate_ls A_eq_dec ns f h mg h' h.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f n h ms) h mg h' h) (@collate_ls A B A_eq_dec ns f h mg h' h) *)
    assert (H_eq: update2 A_eq_dec f n h ms h' h = f h' h).
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
    break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f n h ms) h mg h' h) (@collate_ls A B A_eq_dec ns f h mg h' h) *)
    rewrite (collate_ls_f_eq _ _ _ _ _ _ _ H_eq).
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
    trivial.
  Qed.

  Lemma collate_ls_cases :
    forall s (f : A -> A -> list B) to m a b,
      collate_ls A_eq_dec s f to m a b = f a b \/
      exists l,
        (forall x, In x l -> x = m) /\
        collate_ls A_eq_dec s f to m a b = f a b ++ l.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: or (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (@app B (f a b) l)))) *)
    generalize dependent f.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec s f to m a b) (@app B (f a b) l)))) *)
    induction s as [|n s].
    - auto.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - intros.
      simpl in *.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      destruct (A_eq_dec b to), (A_eq_dec n a); subst.
      + specialize (IHs (update2 A_eq_dec f a to (f a to ++ [m])));
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
          break_or_hyp.
        * find_rewrite.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
          rewrite update2_eq; eauto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
          right; eexists; intuition.
          find_apply_lem_hyp in_inv;
            break_or_hyp;
            [|exfalso]; eauto using in_nil.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
        * break_exists_name l; break_and.
(* Goal: @In B x (f a b) *)
          repeat find_rewrite.
(* Goal: or (@eq (list B) (@app B (@update2 A (list B) A_eq_dec f a to (@app B (f a to) (@cons B m (@nil B))) a to) l) (f a to)) (@ex (list B) (fun l0 : list B => and (forall (x : B) (_ : @In B x l0), @eq B x m) (@eq (list B) (@app B (@update2 A (list B) A_eq_dec f a to (@app B (f a to) (@cons B m (@nil B))) a to) l) (@app B (f a to) l0)))) *)
          rewrite update2_same.
(* Goal: or (@eq (list B) (@app B (@app B (f a to) (@cons B m (@nil B))) l) (f a to)) (@ex (list B) (fun l0 : list B => and (forall (x : B) (_ : @In B x l0), @eq B x m) (@eq (list B) (@app B (@app B (f a to) (@cons B m (@nil B))) l) (@app B (f a to) l0)))) *)
          right; exists (m :: l).
(* Goal: and (forall (x : B) (_ : @In B x (@cons B m l)), @eq B x m) (@eq (list B) (@app B (@app B (f a to) (@cons B m (@nil B))) l) (@app B (f a to) (@cons B m l))) *)
          split.
          -- intros;
               find_apply_lem_hyp in_inv;
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
               intuition.
          -- rewrite <- app_assoc; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      + rewrite collate_ls_neq_update2; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      + rewrite collate_ls_neq_to, update2_diff2; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      + rewrite collate_ls_neq_to, update2_diff2; auto.
  Qed.

  Lemma collate_ls_in_neq_in_before :
    forall s (f : A -> A -> list B) to m a b x,
      In x (collate_ls A_eq_dec s f to m a b) ->
      x <> m ->
      In x (f a b).
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec ns (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg from h) (@app B (f from h) (@cons B mg (@nil B))) *)
    pose proof (collate_ls_cases s f to m a b); break_or_hyp.
    - now find_rewrite.
    - break_exists; break_and.
(* Goal: @In B x (f a b) *)
      find_rewrite.
(* Goal: False *)
    find_apply_lem_hyp in_app_or; break_or_hyp; auto.
(* Goal: @In B x (f a b) *)
    find_apply_hyp_hyp; congruence.
  Qed.

  Lemma collate_ls_not_related :
    forall ns (f : A -> A -> list B) n h mg,
      ~ R h n ->
      collate_ls A_eq_dec (filter_rel R_dec h ns) f h mg n h = f n h.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction ns; intros; simpl in *; auto.
(* Goal: not (@In A a (@app A x x0)) *)
    case (A_eq_dec n a); intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - subst.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
    - break_if; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      simpl.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite IHns; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
      break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
  Qed.

  Lemma collate_ls_not_in_related :
    forall ns (f : A -> A -> list B) n h mg,
      ~ In n ns ->
      collate_ls A_eq_dec (filter_rel R_dec h ns) f h mg n h = f n h.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite collate_ls_not_in; auto.
(* Goal: not (@In A n (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) *)
    apply not_in_not_in_filter_rel.
(* Goal: @Permutation A l (@app A x x0) *)
    assumption.
  Qed.

  Lemma collate_ls_not_in_related_remove_all :
    forall ns (f : A -> A -> list B) n h mg ns',
      ~ In n ns ->
      collate_ls A_eq_dec (filter_rel R_dec h (remove_all A_eq_dec ns' ns)) f h mg n h = f n h.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    rewrite collate_ls_not_in; auto.
(* Goal: not (@In A n (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) *)
    apply not_in_not_in_filter_rel.
(* Goal: not (@In A a (@app A x x0)) *)
    intro.
(* Goal: False *)
    contradict H.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    eapply in_remove_all_was_in; eauto.
  Qed.

  Lemma collate_ls_in_remove_all :
    forall mg n h ns (f : A -> A -> list B) ns',
      In n ns' ->
      collate_ls A_eq_dec (filter_rel R_dec h (remove_all A_eq_dec ns' ns)) f h mg n h = f n h.
  Proof using.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) f h mg n h) (f n h) *)
    revert f.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    induction ns; intros.
    - rewrite remove_all_nil.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
    - pose proof (remove_all_cons A_eq_dec ns' a ns) as H_cn.
(* Goal: @In B x (f a b) *)
      break_or_hyp; break_and; find_rewrite.
      * rewrite IHns.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
        trivial.
      * simpl in *.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
        simpl.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg n h) (f n h) *)
        assert (H_neq: a <> n).
(* Goal: not (@In A a (@app A x x0)) *)
        intro.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
        subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
        intuition.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns)) (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B mg (@nil B)))) h mg n h) (f n h) *)
        rewrite IHns.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
        unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
        break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
        break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
        intuition.
  Qed.

  Lemma collate_ls_app :
    forall l1 l2 (f : A -> A -> list B) h m,
      collate_ls A_eq_dec (l1 ++ l2) f h m = collate_ls A_eq_dec l2 (collate_ls A_eq_dec l1 f h m) h m.
  Proof using. 
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l1; simpl in *; intuition eauto.
  Qed.

  Lemma collate_ls_split_eq :
    forall l1 l2 (f : A -> A -> list B) h m from to,
      h <> from -> 
      collate_ls A_eq_dec (l1 ++ h :: l2) f to m from to =
      collate_ls A_eq_dec  (l1 ++ l2) f to m from to.
  Proof using.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    induction l1; simpl in *; auto.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec l2 (@update2 A (list B) A_eq_dec f h to (@app B (f h to) (@cons B m (@nil B)))) to m from to) (@collate_ls A B A_eq_dec l2 f to m from to) *)
    apply collate_ls_f_eq.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
    unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
    break_if; auto.
(* Goal: @eq (list B) (@app B (f h to) (@cons B m (@nil B))) (f from to) *)
    break_and.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
    intuition.
  Qed.

  Lemma collate_ls_not_in_mid :
    forall h h' l1 l2 (f : A -> A -> list B) m,
      ~ In h' (l1 ++ l2) ->
      collate_ls A_eq_dec (l1 ++ l2) (update2 A_eq_dec f h' h (f h' h ++ [m])) h m = collate_ls A_eq_dec (l1 ++ h' :: l2) f h m.
  Proof using.
(* Goal: forall (h h' : A) (l1 l2 : list A) (f : forall (_ : A) (_ : A), list B) (m : B) (_ : not (@In A h' (@app A l1 l2))), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@app A l1 l2) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A l1 (@cons A h' l2)) f h m) *)
    intros h h' l1 l2 f m H_in.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@app A l1 l2) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A l1 (@cons A h' l2)) f h m) *)
    apply functional_extensionality; intro from.
(* Goal: @eq (forall _ : A, list B) (@collate_ls A B A_eq_dec (@app A l1 l2) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) h m from) (@collate_ls A B A_eq_dec (@app A l1 (@cons A h' l2)) f h m from) *)
    apply functional_extensionality; intro to.
(* Goal: @eq (list B) (@collate A B A_eq_dec h' (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B)))) (@app (prod A B) l1 l2) h' to) (@collate A B A_eq_dec h' f (@app (prod A B) l1 (@cons (prod A B) (@pair A B h m) l2)) h' to) *)
    case (A_eq_dec h' from); intro H_dec; case (A_eq_dec h to); intro H_dec'.
    - rewrite <- H_dec.
      rewrite <- H_dec'.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_ls_not_in; auto.
(* Goal: @eq (list B) (@collate_ls A B A_eq_dec (@cons A a (@filter_rel A R R_dec h (@remove_all A A_eq_dec ns' ns))) f h mg n h) (f n h) *)
      rewrite collate_ls_app; simpl.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (@collate_ls A B A_eq_dec l2 (@update2 A (list B) A_eq_dec (@collate_ls A B A_eq_dec l1 f h m) h' h (@app B (@collate_ls A B A_eq_dec l1 f h m h' h) (@cons B m (@nil B)))) h m h' h) *)
      set (f' := collate_ls _ l1 _ _ _).
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (@app B (@collate_ls A B A_eq_dec l1 f h m h' h) (@cons B m (@nil B))) *)
      rewrite collate_ls_not_in.
      * unfold update2 at 2.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (if sumbool_and (@eq A h' h') (not (@eq A h' h')) (@eq A h h) (not (@eq A h h)) (A_eq_dec h' h') (A_eq_dec h h) then @app B (f' h' h) (@cons B m (@nil B)) else f' h' h) *)
        break_if.
      + unfold f'.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) h' h) (@app B (@collate_ls A B A_eq_dec l1 f h m h' h) (@cons B m (@nil B))) *)
        rewrite collate_ls_not_in.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
        -- unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
           break_if; auto.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
           break_or_hyp; intuition.
        -- intro.
(* Goal: False *)
           contradict H_in.
(* Goal: @In A h' (@app A l1 l2) *)
           apply in_or_app.
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
           left.
(* Goal: @Permutation A l (@app A x x0) *)
           assumption.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      + break_or_hyp; intuition.
        * intro.
(* Goal: False *)
          contradict H_in.
(* Goal: @In A h' (@app A l1 l2) *)
          apply in_or_app.
(* Goal: or (@In A h' l1) (@In A h' l2) *)
          right.
(* Goal: @Permutation A l (@app A x x0) *)
          assumption.
    - rewrite collate_ls_neq_to; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_ls_neq_to; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
    - rewrite H_dec'. 
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_ls_neq_update2; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_ls_split_eq; auto.
    - rewrite collate_ls_neq_to; auto.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_ls_neq_to; auto.
(* Goal: @eq (list B) (@update2 A (list B) A_eq_dec f h' h (@app B (f h' h) (@cons B m (@nil B))) from to) (f from to) *)
      unfold update2.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      break_if; auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      break_and; subst.
(* Goal: @eq (list B) (@app B (f from to) (@cons B m (@nil B))) (f from to) *)
      intuition.
  Qed.

  Lemma NoDup_Permutation_collate_ls_eq :
    forall l (f : A -> A -> list B) h m l',
      NoDup l ->
      Permutation l l' ->
      collate_ls A_eq_dec l f h m = collate_ls A_eq_dec l' f h m.
  Proof using.
(* Goal: forall (l : list A) (f : forall (_ : A) (_ : A), list B) (h : A) (m : B) (l' : list A) (_ : @NoDup A l) (_ : @Permutation A l l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    intros l f h m l'.
(* Goal: forall (_ : @NoDup A l) (_ : @Permutation A l l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    revert f l'.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A l) (_ : @Permutation A l l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    induction l.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - intros.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      find_apply_lem_hyp Permutation_nil.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@nil A) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      subst.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: forall (f : forall (_ : A) (_ : A), list B) (l' : list A) (_ : @NoDup A (@cons A a l)) (_ : @Permutation A (@cons A a l) l'), @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
    - intros.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@cons A a l) f h m) (@collate_ls A B A_eq_dec l' f h m) *)
      invc_NoDup.
      simpl in *.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      assert (H_in: In a (a :: l)).
(* Goal: @In A a (@cons A a l) *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      left.
(* Goal: @eq A a a *)
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      trivial.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      pose proof (Permutation_in _ H0 H_in) as H_pm'.
(* Goal: and (forall (x : B) (_ : @In B x (@cons B m l)), @eq B x m) (@eq (list B) (@app B (@app B (f a to) (@cons B m (@nil B))) l) (@app B (f a to) (@cons B m l))) *)
      find_apply_lem_hyp in_split.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      break_exists.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec l' f h m) *)
      subst_max.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A x (@cons A a x0)) f h m) *)
      find_apply_lem_hyp Permutation_cons_app_inv.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec l (@update2 A (list B) A_eq_dec f a h (@app B (f a h) (@cons B m (@nil B)))) h m) (@collate_ls A B A_eq_dec (@app A x (@cons A a x0)) f h m) *)
      set (f' := update2 _ _ _ _ _).
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite (IHl f' _ H4 H0); auto.
(* Goal: @eq (forall (_ : A) (_ : A), list B) (@collate_ls A B A_eq_dec (@app A x x0) f' h m) (@collate_ls A B A_eq_dec (@app A x (@cons A a x0)) f h m) *)
      unfold f'.
(* Goal: forall f : forall (_ : A) (_ : A), list B, or (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (f a b)) (@ex (list B) (fun l : list B => and (forall (x : B) (_ : @In B x l), @eq B x m) (@eq (list B) (@collate_ls A B A_eq_dec (@nil A) f to m a b) (@app B (f a b) l)))) *)
      rewrite collate_ls_not_in_mid; auto.
(* Goal: not (@In A a (@app A x x0)) *)
      intro.
(* Goal: False *)
      contradict H3.
(* Goal: @In A a l *)
      revert H.
(* Goal: forall _ : @In A a (@app A x x0), @In A a l *)
      apply Permutation_in.
(* Goal: @Permutation A (@app A x x0) l *)
      apply Permutation_sym.
(* Goal: @Permutation A l (@app A x x0) *)
      assumption.
  Qed.

End Update2Rel.
