Require Import Arith.
Require Import Omega.
Require Import List.
Import ListNotations.
Require Import Sorting.Permutation.
Require Import StructTact.StructTactics.
Require Import StructTact.ListTactics.

Set Implicit Arguments.

Notation member := (in_dec eq_nat_dec).

Lemma seq_range :
  forall n a x,
    In x (seq a n) ->
    a <= x < a + n.
Proof.
(* Goal: forall (n a x : nat) (_ : @In nat x (seq a n)), and (le a x) (lt x (Init.Nat.add a n)) *)
  induction n; intros; simpl in *.
  - intuition.
  - break_or_hyp; try find_apply_hyp_hyp; intuition.
Qed.

Lemma plus_gt_0 :
  forall a b,
    a + b > 0 ->
    a > 0 \/ b > 0.
Proof.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
  intros.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
  destruct (eq_nat_dec a 0); intuition.
Qed.

Section list_util.
  Variables A B C : Type.
  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.

  Lemma list_neq_cons :
    forall (l : list A) x,
      x :: l <> l.
  Proof using.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    intuition.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@nil A) (@app A l1 l2)) (and (@eq (list B) (@map A B f l1) xs) (@eq (list B) (@map A B f l2) ys)))) *)
    symmetry in H.
    induction l;
      now inversion H.
  Qed.

  Lemma remove_preserve :
    forall (x y : A) xs,
      x <> y ->
      In y xs ->
      In y (remove A_eq_dec x xs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - intuition.
    - simpl in *.
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
      concludes.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      intuition; break_if; subst; try congruence; intuition.
  Qed.

  Lemma in_remove :
    forall (x y : A) xs,
      In y (remove A_eq_dec x xs) ->
      In y xs.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl in *. break_if; simpl in *; intuition.
  Qed.

  Lemma remove_partition :
    forall xs (p : A) ys,
      remove A_eq_dec p (xs ++ p :: ys) = remove A_eq_dec p (xs ++ ys).
  Proof using.
(* Goal: forall (xs : list A) (p : A) (ys : list A), @eq (list A) (@remove A A_eq_dec p (@app A xs (@cons A p ys))) (@remove A A_eq_dec p (@app A xs ys)) *)
    induction xs; intros; simpl; break_if; congruence.
  Qed.

  Lemma remove_not_in :
    forall (x : A) xs,
      ~ In x xs ->
      remove A_eq_dec x xs = xs.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros. induction xs; simpl in *; try break_if; intuition congruence.
  Qed.

  Lemma remove_app_comm :
    forall a xs ys,
      remove A_eq_dec a (xs ++ ys) = remove A_eq_dec a xs ++ remove A_eq_dec a ys.
  Proof.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq (list A) (@remove A A_eq_dec a (@app A xs ys)) (@app A (@remove A A_eq_dec a xs) (@remove A A_eq_dec a ys)) *)
    generalize dependent ys.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - tauto.
    - destruct (A_eq_dec a0 a);
      simpl;
      break_if;
      try rewrite <- app_comm_cons;
      rewrite IHxs; 
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
      congruence.
  Qed.

  Lemma filter_app : forall (f : A -> bool) xs ys,
      filter f (xs ++ ys) = filter f xs ++ filter f ys.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl. rewrite IHxs. break_if; auto.
  Qed.

  Lemma filter_fun_ext_eq : forall f g xs,
      (forall a : A, In a xs -> f a = g a) ->
      filter f xs = filter g xs.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl. rewrite H by intuition. rewrite IHxs by intuition. auto.
  Qed.

  Lemma not_in_filter_false :
    forall (f : A -> bool) l x,
      In x l ->
      ~ In x (filter f l) ->
      f x = false.
  Proof.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq bool (f x) false *)
    destruct (f x) eqn:?H; [|tauto].
(* Goal: @eq bool true false *)
    unfold not in *; find_false.
(* Goal: @In A x (@filter A f l) *)
    now eapply filter_In.
  Qed.

  Lemma filter_length_bound :
    forall f (l : list A),
      length (filter f l) <= length l.
  Proof.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) l acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y l) (@eq A x (g y)))) *)
    induction l.
    - easy.
    - simpl.
(* Goal: le (@length A (if f a then @cons A a (@filter A f l) else @filter A f l)) (S (@length A l)) *)
      break_if; simpl; omega.
  Qed.

  Lemma NoDup_map_injective : forall (f : A -> B) xs,
      (forall x y, In x xs -> In y xs ->
              f x = f y -> x = y) ->
      NoDup xs -> NoDup (map f xs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - constructor.
    - simpl. invc_NoDup. constructor.
      + intro. do_in_map.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
        assert (x = a) by intuition.
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
        congruence.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      + intuition.
  Qed.

  Lemma NoDup_disjoint_append :
    forall (l : list A) l',
      NoDup l ->
      NoDup l' ->
      (forall a, In a l -> ~ In a l') ->
      NoDup (l ++ l').
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction l; intros.
    - auto.
    - simpl. invc_NoDup. constructor.
      + intro. do_in_app. intuition eauto with *.
      + intuition eauto with *.
  Qed.

  Lemma NoDup_map_partition :
    forall (f : A -> B) xs l y zs xs' y' zs',
      NoDup (map f l) ->
      l = xs ++ y :: zs ->
      l = xs' ++ y' :: zs' ->
      f y = f y' ->
      xs = xs'.
  Proof using.
(* Goal: forall (f : forall _ : A, B) (xs l : list A) (y : A) (zs xs' : list A) (y' : A) (zs' : list A) (_ : @NoDup B (@map A B f l)) (_ : @eq (list A) l (@app A xs (@cons A y zs))) (_ : @eq (list A) l (@app A xs' (@cons A y' zs'))) (_ : @eq B (f y) (f y')), @eq (list A) xs xs' *)
    induction xs; simpl; intros; destruct xs'.
    - auto.
    - subst. simpl in *. find_inversion.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
      invc H. exfalso. rewrite map_app in *. simpl in *.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      repeat find_rewrite. intuition.
    - subst. simpl in *. find_inversion.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
      invc H. exfalso. rewrite map_app in *. simpl in *.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      repeat find_rewrite. intuition.
    - subst. simpl in *. find_injection. intros. subst.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      f_equal. eapply IHxs; eauto. solve_by_inversion.
  Qed.

  Lemma filter_NoDup :
    forall p (l : list A),
      NoDup l ->
      NoDup (filter p l).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction l; intros.
    - auto.
    - invc_NoDup. simpl. break_if; auto.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      constructor; auto.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      intro. apply filter_In in H. intuition.
  Qed.

  Lemma NoDup_map_filter :
    forall (f : A -> B) g l,
      NoDup (map f l) ->
      NoDup (map f (filter g l)).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros. induction l; simpl in *.
    - constructor.
    - invc_NoDup. concludes.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      break_if; simpl in *; auto.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      constructor; auto.
(* Goal: not (or (@eq A (@fst A B a) n) (@In A n (@map (prod A B) A (@fst A B) l))) *)
      intro. do_in_map.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      find_apply_lem_hyp filter_In. intuition.
      match goal with | H : _ -> False |- False => apply H end.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      apply in_map_iff. eauto.
  Qed.

  Lemma filter_true_id : forall (f : A -> bool) xs,
      (forall x, In x xs -> f x = true) ->
      filter f xs = xs.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl. now rewrite H, IHxs by intuition.
  Qed.

  Lemma map_of_map : forall (f : A -> B) (g : B -> C) xs,
      map g (map f xs) = map (fun x => g (f x)) xs.
  Proof using.
(* Goal: forall (f : forall _ : A, B) (g : forall _ : B, C) (xs : list A), @eq (list C) (@map B C g (@map A B f xs)) (@map A C (fun x : A => g (f x)) xs) *)
    induction xs; simpl; auto using f_equal2.
  Qed.

  Lemma filter_except_one : forall (f g : A -> bool) x xs,
      (forall y, In y xs ->
            x <> y ->
            f y = g y) ->
      g x = false ->
      filter f (remove A_eq_dec x xs) = filter g xs.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl.
(* Goal: ge (@length A (if A_eq_dec x a then @remove A A_eq_dec x xs else @cons A a (@remove A A_eq_dec x xs))) (Init.Nat.sub (@length A xs) O) *)
      break_if.
      + subst. repeat find_rewrite. eauto with *.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@app A (@map (prod A B) A (@fst A B) x) (@map (prod A B) A (@fst A B) (@cons (prod A B) a x0))) *)
      + simpl. rewrite H by auto with *.
(* Goal: @eq (list A) (if g a then @cons A a (@filter A f (@remove A A_eq_dec x xs)) else @filter A f (@remove A A_eq_dec x xs)) (if g a then @cons A a (@filter A g xs) else @filter A g xs) *)
        break_if; eauto using f_equal2 with *.
  Qed.

  Lemma flat_map_nil : forall (f : A -> list B) l,
      flat_map f l = [] ->
      l = [] \/ (forall x, In x l -> f x = []).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction l; intros.
    - intuition.
    - right. simpl in *.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@nil A) (@app A l1 l2)) (and (@eq (list B) (@map A B f l1) xs) (@eq (list B) (@map A B f l2) ys)))) *)
      apply app_eq_nil in H.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      intuition; subst; simpl in *; intuition.
  Qed.

  Theorem NoDup_Permutation_NoDup :
    forall (l l' : list A),
      NoDup l ->
      Permutation l l' ->
      NoDup l'.
  Proof using.
(* Goal: forall (l l' : list A) (_ : @NoDup A l) (_ : @Permutation A l l'), @NoDup A l' *)
    intros l l' Hnd Hp.
    induction Hp; auto; invc_NoDup; constructor;
      eauto using Permutation_in, Permutation_sym;
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      simpl in *; intuition.
  Qed.

  Theorem NoDup_append :
    forall l (a : A),
      NoDup (l ++ [a]) <-> NoDup (a :: l).
  Proof using. 
(* Goal: forall (l : list A) (a : A), iff (@NoDup A (@app A l (@cons A a (@nil A)))) (@NoDup A (@cons A a l)) *)
    intuition eauto using NoDup_Permutation_NoDup, Permutation_sym, Permutation_cons_append.
  Qed.

  Lemma NoDup_map_elim :
    forall (f : A -> B) xs x y,
      f x = f y ->
      NoDup (map f xs) ->
      In x xs ->
      In y xs ->
      x = y.
  Proof using.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    induction xs; intros; simpl in *.
    - intuition.
    - invc_NoDup. intuition; subst; auto; exfalso.
      + repeat find_rewrite. auto using in_map.
      + repeat find_reverse_rewrite. auto using in_map.
  Qed.

  Lemma remove_length_not_in : forall (x : A) xs,
      ~ In x xs ->
      length (remove A_eq_dec x xs) = length xs.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl in *. intuition.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      break_if; subst; simpl; intuition.
  Qed.

  Lemma remove_length_in : forall (x : A) xs,
      In x xs ->
      NoDup xs ->
      S (length (remove A_eq_dec x xs)) = length xs.
  Proof using.
    induction xs; intros; simpl in *; intuition; invc_NoDup;
      break_if; subst; intuition (simpl; try congruence).
(* Goal: @eq nat (S (@length A (@remove A A_eq_dec x xs))) (S (@length A xs)) *)
    now rewrite remove_length_not_in.
  Qed.

  Lemma subset_size_eq :
    forall xs,
      NoDup xs ->
      forall ys,
        NoDup ys ->
        (forall x : A, In x xs -> In x ys) ->
        length xs = length ys ->
        (forall x, In x ys -> In x xs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - destruct ys; simpl in *; congruence.
    - invc_NoDup. concludes.
(* Goal: False *)
      assert (In a ys) by eauto with *.

(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_apply_lem_hyp in_split.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
      break_exists_name l1.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
      break_exists_name l2.
(* Goal: and (@eq (list A) (@cons A a l) (@app A (@cons A a l1) l2)) (and (@eq (list B) (@map A B f (@cons A a l1)) (@cons B (f a) xs)) (@eq (list B) (@map A B f l2) ys)) *)
      subst.

      specialize (IHxs (l1 ++ l2)).

(* Goal: @In A x (@cons A a xs) *)
      conclude_using ltac:(eauto using NoDup_remove_1).

(* Goal: ge (@length A ys) (@length A (@cons A a xs)) *)
      forward IHxs.
(* Goal: forall (x : A) (_ : @In A x xs), @In A x (@app A l1 l2) *)
(* Goal: @In A x (@cons A a xs) *)
      intros x' Hx'.
      assert (In x' (l1 ++ a :: l2)) by eauto with *.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      do_in_app. simpl in *. intuition. subst. congruence.
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
      concludes.

(* Goal: ge (@length A ys) (@length A (@cons A a xs)) *)
      forward IHxs.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
      rewrite app_length in *. simpl in *. omega.
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
      concludes.

(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      do_in_app. simpl in *. intuition.
  Qed.

  Lemma remove_NoDup :
    forall (x : A) xs,
      NoDup xs ->
      NoDup (remove A_eq_dec x xs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto with struct_util.
    - invc_NoDup. simpl. break_if; eauto 6 using in_remove with struct_util.
  Qed.

  Lemma remove_length_ge : forall (x : A) xs,
      NoDup xs ->
      length (remove A_eq_dec x xs) >= length xs - 1.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - invc_NoDup. simpl. break_if.
      + rewrite <- minus_n_O.
(* Goal: and (@eq (list A) (@cons A a l) (@app A (@cons A a l1) l2)) (and (@eq (list B) (@map A B f (@cons A a l1)) (@cons B (f a) xs)) (@eq (list B) (@map A B f l2) ys)) *)
        subst.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
        rewrite remove_length_not_in; auto.
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
      + simpl. concludes. omega.
  Qed.

  Lemma remove_length_le :
    forall (x : A) xs eq_dec,
      length xs >= length (remove eq_dec x xs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - auto.
    - simpl in *.
(* Goal: ge (S (@length A xs)) (@length A (if eq_dec x a then @remove A eq_dec x xs else @cons A a (@remove A eq_dec x xs))) *)
      specialize (IHxs eq_dec).
(* Goal: ge (@length A ys) (S (@length A xs)) *)
      break_if; subst; simpl; omega.
  Qed.

  Lemma remove_length_lt :
    forall (x : A) xs eq_dec,
      In x xs ->
      length xs > length (remove eq_dec x xs).
  Proof using.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    induction xs; intros; simpl in *; intuition.
    - subst.
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
      break_if; try congruence.
(* Goal: gt (S (@length A xs)) (@length A (@remove A eq_dec x xs)) *)
      pose proof remove_length_le x xs eq_dec.
(* Goal: ge (@length A ys) (S (@length A xs)) *)
      omega.
    - specialize (IHxs ltac:(eauto) ltac:(eauto)).
(* Goal: ge (@length A ys) (S (@length A xs)) *)
      break_if; subst; simpl; omega.
  Qed.

  Lemma subset_length :
    forall xs ys,
      NoDup xs ->
      (forall x : A, In x xs -> In x ys) ->
      length ys >= length xs.
  Proof using A_eq_dec.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    induction xs; intros.
    - simpl. omega.
    - specialize (IHxs (remove A_eq_dec a ys)).
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
      invc_NoDup.
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
      concludes.

(* Goal: ge (@length A ys) (@length A (@cons A a xs)) *)
      forward IHxs.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
      intros.
(* Goal: @In A x (@remove A A_eq_dec a ys) *)
(* Goal: ge (@length A ys) (@length A (@cons A a xs)) *)
      apply remove_preserve; [congruence|intuition].
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
      concludes.

(* Goal: ge (@length A ys) (@length A (@cons A a xs)) *)
      pose proof remove_length_lt a ys A_eq_dec.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      conclude_using intuition.

(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@app A (@map (prod A B) A (@fst A B) x) (@map (prod A B) A (@fst A B) (@cons (prod A B) a x0))) *)
      simpl. omega.
  Qed.

  Lemma app_cons_singleton_inv :
    forall xs (y : A) zs w,
      xs ++ y :: zs = [w] ->
      xs = [] /\ y = w /\ zs = [].
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: and (@eq (list A) xs (@nil A)) (and (@eq A y w) (@eq (list A) zs (@nil A))) *)
    destruct xs.
    - solve_by_inversion.
    - destruct xs; solve_by_inversion.
  Qed.

  Lemma app_cons_in :
    forall (l : list A) xs a ys,
      l = xs ++ a :: ys ->
      In a l.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros. subst. auto with *.
  Qed.
  Hint Resolve app_cons_in : struct_util.

  Lemma app_cons_in_rest:
    forall (l : list A) xs a b ys,
      l = xs ++ a :: ys ->
      In b (xs ++ ys) ->
      In b l.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros. subst. in_crush.
  Qed.
  Hint Resolve app_cons_in_rest : struct_util.

  Lemma in_rest_app_cons:
    forall (l xs ys : list A) a b,
      l = xs ++ a :: ys ->
      In b l ->
      a <> b ->
      In b (xs ++ ys).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @In A b (@app A xs ys) *)
    subst_max.
(* Goal: @In A b (@app A xs ys) *)
    do_in_app.
(* Goal: False *)
    break_or_hyp.
    - auto with datatypes.
    - find_apply_lem_hyp in_inv.
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
      break_or_hyp; auto using in_or_app || congruence.
  Qed.
  Hint Resolve in_rest_app_cons : struct_util.

  Lemma remove_filter_commute :
    forall (l : list A) A_eq_dec f x,
      remove A_eq_dec x (filter f l) = filter f (remove A_eq_dec x l).
  Proof using.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l; intros; simpl in *; auto.
(* Goal: @eq (list A) (@remove A A_eq_dec0 x (if f a then @cons A a (@filter A f l) else @filter A f l)) (@filter A f (if A_eq_dec0 x a then @remove A A_eq_dec0 x l else @cons A a (@remove A A_eq_dec0 x l))) *)
    repeat (break_if; subst; simpl in *; try congruence).
  Qed.

  Lemma In_filter_In :
    forall (f : A -> bool) x l l',
      filter f l = l' ->
      In x l' -> In x l.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros. subst.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    eapply filter_In; eauto.
  Qed.

  Lemma filter_partition :
    forall (l1 : list A) f l2 x l1' l2',
      NoDup (l1 ++ x :: l2) ->
      filter f (l1 ++ x :: l2) = (l1' ++ x :: l2') ->
      filter f l1 = l1' /\ filter f l2 = l2'.
  Proof using.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
    induction l1; intros; simpl in *; break_if; simpl in *; invc_NoDup.
    - destruct l1'; simpl in *.
      + solve_by_inversion.
      + find_inversion. exfalso. eauto using In_filter_In with *.
    - exfalso. eauto using In_filter_In with *.
    - destruct l1'; simpl in *; break_and; find_inversion.
      + exfalso. eauto with *.
      + find_apply_hyp_hyp. intuition auto using f_equal2.
    - eauto.
  Qed.

  Lemma map_inverses :
    forall (la : list A) (lb : list B)  (f : A -> B) g,
      (forall a, g (f a) = a) ->
      (forall b, f (g b) = b) ->
      lb = map f la ->
      la = map g lb.
  Proof using.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    destruct la; intros; simpl in *.
    - subst. reflexivity.
    - destruct lb; try congruence.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
      simpl in *. find_inversion.
(* Goal: @eq (list A) (@cons A a la) (@cons A (g (f a)) (@map B A g (@map A B f la))) *)
      find_higher_order_rewrite.
(* Goal: @eq (list A) (@cons A a la) (@cons A a (@map B A g (@map A B f la))) *)
      f_equal.
(* Goal: @eq (list A) la (@map B A g (@map A B f la)) *)
      rewrite map_map.
(* Goal: @eq (list A) la (@map A A (fun x : A => g (f x)) la) *)
      erewrite map_ext; [symmetry; apply map_id|].
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
      simpl in *. auto.
  Qed.

  Lemma In_notIn_implies_neq :
    forall x y l,
      In(A:=A) x l ->
      ~ In(A:=A) y l ->
      x <> y.
  Proof using.
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
    intuition congruence.
  Qed.

  Lemma In_cons_neq :
    forall a x xs,
      In(A:=A) a (x :: xs) ->
      a <> x ->
      In a xs.
  Proof using.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@app A (@map (prod A B) A (@fst A B) x) (@map (prod A B) A (@fst A B) (@cons (prod A B) a x0))) *)
    simpl.
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
    intuition congruence.
  Qed.

  Lemma NoDup_app3_not_in_1 :
    forall (xs ys zs : list A) b,
      NoDup (xs ++ ys ++ b :: zs) ->
      In b xs ->
      False.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
    rewrite <- app_ass in *.
(* Goal: False *)
    find_apply_lem_hyp NoDup_remove.
(* Goal: False *)
    rewrite app_ass in *.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    intuition.
  Qed.

  Lemma NoDup_app3_not_in_2 :
    forall (xs ys zs : list A) b,
      NoDup (xs ++ ys ++ b :: zs) ->
      In b ys ->
      False.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
    rewrite <- app_ass in *.
(* Goal: False *)
    find_apply_lem_hyp NoDup_remove_2.
(* Goal: False *)
    rewrite app_ass in *.
(* Goal: False *)
    auto 10 with *.
  Qed.

  Lemma NoDup_app3_not_in_3 :
    forall (xs ys zs : list A) b,
      NoDup (xs ++ ys ++ b :: zs) ->
      In b zs ->
      False.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
    rewrite <- app_ass in *.
(* Goal: False *)
    find_apply_lem_hyp NoDup_remove_2.
(* Goal: False *)
    rewrite app_ass in *.
(* Goal: False *)
    auto 10 with *.
  Qed.

  Lemma In_cons_2_3 :
    forall xs ys zs x y a,
      In (A:=A) a (xs ++ ys ++ zs) ->
      In a (xs ++ x :: ys ++ y :: zs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @In A a (@app A xs (@cons A x (@app A ys (@cons A y zs)))) *)
    repeat (do_in_app; intuition auto 10 with *).
  Qed.

  Lemma In_cons_2_3_neq :
    forall a x y xs ys zs,
      In (A:=A) a (xs ++ x :: ys ++ y :: zs) ->
      a <> x ->
      a <> y ->
      In a (xs ++ ys ++ zs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @In A a (@app A xs (@app A ys zs)) *)
    repeat (do_in_app; simpl in *; intuition (auto with *; try congruence)).
  Qed.

  Lemma in_middle_reduce :
    forall a xs y zs,
      In (A:=A) a (xs ++ y :: zs) ->
      a <> y ->
      In a (xs ++ zs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    do_in_app; simpl in *; intuition. congruence.
  Qed.

  Lemma in_middle_insert :
    forall a xs y zs,
      In (A:=A) a (xs ++ zs) ->
      In a (xs ++ y :: zs).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    do_in_app; simpl in *; intuition.
  Qed.

  Lemma NoDup_rev :
    forall l,
      NoDup (A:=A) l ->
      NoDup (rev l).
  Proof using.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@app A (@map (prod A B) A (@fst A B) x) (@map (prod A B) A (@fst A B) (@cons (prod A B) a x0))) *)
    induction l; intros; simpl.
    - auto.
    - apply NoDup_append.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
      invc_NoDup.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      constructor; auto.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      intuition.
(* Goal: False *)
      find_apply_lem_hyp in_rev.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      auto.
  Qed.

  Lemma NoDup_map_map :
    forall (f : A -> B) (g : A -> C) xs,
      (forall x y, In x xs -> In y xs -> f x = f y -> g x = g y) ->
      NoDup (map g xs) ->
      NoDup (map f xs).
  Proof using.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    induction xs; intros; simpl in *.
    - constructor.
    - invc_NoDup.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      constructor; auto.
(* Goal: not (or (@eq A (@fst A B a) n) (@In A n (@map (prod A B) A (@fst A B) l))) *)
      intro.
(* Goal: False *)
      do_in_map.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_apply_hyp_hyp.
(* Goal: False *)
      find_reverse_rewrite.
(* Goal: False *)
      auto using in_map.
  Qed.

  Lemma pigeon :
    forall (l : list A) sub1 sub2,
      (forall a, In a sub1 -> In a l) ->
      (forall a, In a sub2 -> In a l) ->
      NoDup l ->
      NoDup sub1 ->
      NoDup sub2 ->
      length sub1 + length sub2 > length l ->
      exists a, In a sub1 /\ In a sub2.
  Proof using A_eq_dec.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) l acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y l) (@eq A x (g y)))) *)
    induction l.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    + simpl in *. find_apply_lem_hyp plus_gt_0. intuition.
      * destruct sub1; simpl in *; [omega|].
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
        specialize (H a). intuition.
      * destruct sub2; simpl in *; [omega|].
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
        specialize (H0 a). intuition.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    + intros. simpl in *.
      destruct (in_dec A_eq_dec a sub1);
        destruct (in_dec A_eq_dec a sub2); eauto;
          specialize (IHl (remove A_eq_dec a sub1) (remove A_eq_dec a sub2));
          cut (exists a0, In a0 (remove A_eq_dec a sub1) /\ In a0 (remove A_eq_dec a sub2));
          try solve [intros; break_exists;
                     intuition eauto using in_remove];
          apply IHl; try solve [
                           intros; find_copy_apply_lem_hyp in_remove;
                           find_apply_hyp_hyp; intuition; subst; exfalso; eapply remove_In; eauto];
          eauto using remove_NoDup; try solve_by_inversion;
            repeat match goal with
                   | H : ~ In a ?sub |- _ =>
                     assert (length (remove A_eq_dec a sub) = length sub)
                       by eauto using remove_length_not_in; clear H
                   | H : In a ?sub |- _ =>
                     assert (length (remove A_eq_dec a sub) >= length sub - 1)
                       by eauto using remove_length_ge; clear H
(* Goal: ge (@length A ys) (S (@length A xs)) *)
                   end; omega.
  Qed.

  Lemma snoc_assoc :
    forall (l : list A) x y,
      l ++ [x; y] = (l ++ [x]) ++ [y].
  Proof using.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    induction l; intros; simpl; intuition.
(* Goal: @eq (list A) (@cons A a la) (@cons A a (@map B A g (@map A B f la))) *)
    auto using f_equal.
  Qed.

  Lemma cons_cons_app :
    forall (x y : A),
      [x; y] = [x] ++ [y].
  Proof using.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    auto.
  Qed.

  Lemma map_eq_inv :
    forall (f : A -> B) l xs ys,
      map f l = xs ++ ys ->
      exists l1 l2,
        l = l1 ++ l2 /\
        map f l1 = xs /\
        map f l2 = ys.
  Proof using.
(* Goal: forall (f : forall _ : A, B) (l : list A) (xs ys : list B) (_ : @eq (list B) (@map A B f l) (@app B xs ys)), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (and (@eq (list B) (@map A B f l1) xs) (@eq (list B) (@map A B f l2) ys)))) *)
    induction l; simpl; intros xs ys H.
    - symmetry in H. apply app_eq_nil in H. break_and. subst.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      exists [], []. auto.
    - destruct xs; simpl in *.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
      + exists [], (a :: l). intuition.
      + invc H. find_apply_hyp_hyp.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
        break_exists_name l1.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
        break_exists_name l2.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
        break_and.
(* Goal: and (@eq (list A) (@cons A a l) (@app A (@cons A a l1) l2)) (and (@eq (list B) (@map A B f (@cons A a l1)) (@cons B (f a) xs)) (@eq (list B) (@map A B f l2) ys)) *)
        exists (a :: l1), l2. subst.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
        intuition.
  Qed.

  Lemma map_partition :
    forall p l (x : B) p' (f : A -> B),
      map f l = (p ++ x :: p') ->
      exists ap a ap',
        l = ap ++ a :: ap' /\
        map f ap = p /\
        f a = x /\
        map f ap' = p'.
  Proof using.
(* Goal: forall (p : list B) (l : list A) (x : B) (p' : list B) (f : forall _ : A, B) (_ : @eq (list B) (@map A B f l) (@app B p (@cons B x p'))), @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
    intros p l x p' f H_m.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
    pose proof map_eq_inv f _ _ _ H_m.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
    break_exists_name l1.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
    break_exists_name l2.
(* Goal: @ex (list A) (fun ap : list A => @ex A (fun a : A => @ex (list A) (fun ap' : list A => and (@eq (list A) l (@app A ap (@cons A a ap'))) (and (@eq (list B) (@map A B f ap) p) (and (@eq B (f a) x) (@eq (list B) (@map A B f ap') p')))))) *)
    break_and.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
    find_rewrite.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    destruct l2; simpl in *.
    - match goal with H : [] = _ :: _ |- _ => contradict H end.
(* Goal: not (@eq (list B) (@nil B) (@cons B x p')) *)
      auto with datatypes.
    - repeat find_rewrite.
(* Goal: @eq (list A) (@cons A a l) (@cons A a0 l') *)
      find_inversion.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      exists l1, a, l2. auto.
  Qed.

  Lemma map_eq_inv_eq :
    forall (f : A -> B),
      (forall a a', f a = f a' -> a = a') ->
      forall l l', map f l = map f l' -> l = l'.
  Proof using.
(* Goal: @ex (list A) (fun tl : list A => @eq (list A) (@nil A) (@cons A x tl)) *)
    induction l; simpl; intros l' Heq; destruct l'; simpl in *; try congruence.
(* Goal: @eq (list A) (@cons A a l) (@cons A a0 l') *)
    find_inversion. auto using f_equal2.
  Qed.

  Lemma map_fst_snd_id :
    forall l, map (fun t : A * B => (fst t, snd t)) l = l.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
    rewrite <- map_id.
(* Goal: @eq (list (prod A B)) (@map (prod A B) (prod A B) (fun t : prod A B => @pair A B (@fst A B t) (@snd A B t)) l) (@map (prod A B) (prod A B) (fun x : prod A B => x) l) *)
    apply map_ext.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    destruct a; auto.
  Qed.

  Lemma in_firstn : forall n (x : A) xs,
      In x (firstn n xs) -> In x xs.
  Proof using.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    induction n; simpl; intuition; break_match; simpl in *; intuition.
  Qed.

  Lemma firstn_NoDup : forall n (xs : list A),
    NoDup xs ->
    NoDup (firstn n xs).
  Proof using.
(* Goal: @NoDup A (@remove A A_eq_dec x (@nil A)) *)
    induction n; intros; simpl; destruct xs; auto with struct_util.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
    invc_NoDup.
(* Goal: @NoDup A (@cons A a (@firstn A n xs)) *)
    eauto 6 using in_firstn with struct_util.
  Qed.

  Lemma NoDup_mid_not_in :
    forall (a : A) (l l' : list A),
    NoDup (l ++ a :: l') ->
    ~ In a (l ++ l').
  Proof using.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    induction l; intros; simpl in *.
    - invc_NoDup; auto.
    - invc_NoDup.
(* Goal: not (or (@eq A (@fst A B a) n) (@In A n (@map (prod A B) A (@fst A B) l))) *)
      intro.
(* Goal: False *)
      break_or_hyp.
      * match goal with H: ~ In _ _ |- _ => contradict H end.
(* Goal: @In A a (@app A l l') *)
        apply in_or_app.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
        right; left. auto.
      * match goal with H: In _ _ |- _ => contradict H end.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
        eauto.
    Qed.

  Lemma Permutation_split :
    forall (ns ns' : list A) (n : A),
      Permutation (n :: ns) ns' ->
      exists ns0, exists ns1, ns' = ns0 ++ n :: ns1.
  Proof using.
(* Goal: forall (ns ns' : list A) (n : A) (_ : @Permutation A (@cons A n ns) ns'), @ex (list A) (fun ns0 : list A => @ex (list A) (fun ns1 : list A => @eq (list A) ns' (@app A ns0 (@cons A n ns1)))) *)
    intros l l' a H_pm.
(* Goal: not (@eq (list B) (@nil B) (@cons B x p')) *)
    assert (In a (a :: l)); auto with datatypes.
(* Goal: @ex (list A) (fun ns0 : list A => @ex (list A) (fun ns1 : list A => @eq (list A) l' (@app A ns0 (@cons A a ns1)))) *)
    assert (In a l'); eauto using Permutation_in.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    find_apply_lem_hyp In_split; auto.
  Qed.

  Lemma NoDup_app_left :
    forall (l l' : list A),
      NoDup (l ++ l') -> NoDup l.
  Proof using.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    induction l; intros; simpl in *.
    - apply NoDup_nil.
    - invc_NoDup.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_apply_hyp_hyp.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      apply NoDup_cons; auto.
(* Goal: not (or (@eq A (@fst A B a) n) (@In A n (@map (prod A B) A (@fst A B) l))) *)
      intro.
      match goal with H: ~ In _ _ |- _ => contradict H end.
(* Goal: @In A a (@app A l l') *)
      apply in_or_app.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      left; auto.
  Qed.

  Lemma NoDup_app_right :
    forall (l l' : list A),
      NoDup (l ++ l') -> NoDup l'.
  Proof using.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l; intros; simpl in *; auto.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
    invc_NoDup.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    find_apply_hyp_hyp; auto.
  Qed.

  Lemma NoDup_in_not_in_right :
    forall (l l' : list A) (a : A),
      NoDup (l ++ l') -> In a l -> ~ In a l'.
  Proof using.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l; intros; simpl in *; auto.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
    invc_NoDup.
(* Goal: not (@eq (list B) (@nil B) (@cons B x p')) *)
    break_or_hyp; eauto with datatypes.
  Qed.

  Lemma NoDup_in_not_in_left :
    forall (l l' : list A) (a : A),
    NoDup (l ++ l') -> In a l' -> ~ In a l.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l; simpl in *; auto.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
    invc_NoDup.
(* Goal: not (or (@eq A a0 a) (@In A a l)) *)
    concludes.
(* Goal: not (or (@eq A (@fst A B a) n) (@In A n (@map (prod A B) A (@fst A B) l))) *)
    intro.
(* Goal: not (@eq (list B) (@nil B) (@cons B x p')) *)
    break_or_hyp; auto with datatypes.
  Qed.

  Lemma count_occ_app :
    forall l l' (a : A),
      count_occ A_eq_dec (l ++ l') a = count_occ A_eq_dec l a + count_occ A_eq_dec l' a.
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l; simpl in *; auto.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    break_if; auto.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
    find_rewrite.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    auto.
  Qed.

  Lemma Permutation_map_fst :
    forall l l' : list (A * B),
      Permutation l l' ->
      Permutation (map fst l) (map fst l').
  Proof using.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    induction l; intros; simpl in *.
    - find_apply_lem_hyp Permutation_nil.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_rewrite.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      auto.
    - assert (In a l').
(* Goal: not (@eq (list B) (@nil B) (@cons B x p')) *)
        apply Permutation_in with (l := a :: l); auto with datatypes.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_apply_lem_hyp in_split.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      break_exists.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_rewrite.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_apply_lem_hyp Permutation_cons_app_inv.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_apply_hyp_hyp.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) l') *)
      find_rewrite.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@map (prod A B) A (@fst A B) (@app (prod A B) x (@cons (prod A B) a x0))) *)
      rewrite map_app.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@app A (@map (prod A B) A (@fst A B) x) (@map (prod A B) A (@fst A B) (@cons (prod A B) a x0))) *)
      simpl.
(* Goal: @Permutation A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) l)) (@app A (@map (prod A B) A (@fst A B) x) (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) x0))) *)
      apply Permutation_cons_app.
      rewrite <- map_app.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      auto.
     Qed.

  Lemma snd_eq_not_in_map :
    forall (l : list (A * B)) n m,
      (forall nm, In nm l -> snd nm = m) ->
      ~ In (n, m) l ->
      ~ In n (map fst l).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l; simpl in *; auto.
(* Goal: not (or (@eq A (@fst A B a) n) (@In A n (@map (prod A B) A (@fst A B) l))) *)
    intro.
(* Goal: False *)
    break_or_hyp.
    - match goal with H: ~ _ |- _ => contradict H end.
(* Goal: or (@eq (prod A B) a (@pair A B (@fst A B a) m)) (@In (prod A B) (@pair A B (@fst A B a) m) l) *)
      left.
(* Goal: not (@In A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
      destruct a.
      match goal with H: forall _ : A * B, _ |- _ => specialize (H (a, b)) end.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
      simpl in *.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      intuition eauto; repeat find_rewrite; auto.
    - match goal with H: In _ _ |- _ => contradict H end.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      apply IHl; eauto.
  Qed.

  Lemma NoDup_map_snd_fst :
    forall nms : list (A * B),
      NoDup nms ->
      (forall nm nm', In nm nms -> In nm' nms -> snd nm = snd nm') ->
      NoDup (map fst nms).
  Proof using.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    induction nms; simpl in *.
    - apply NoDup_nil.
    - invc_NoDup.
(* Goal: @NoDup A (@cons A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
      apply NoDup_cons.
      * assert (forall nm, In nm nms -> snd nm = snd a).
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
          intuition eauto.
(* Goal: not (@In A (@fst A B a) (@map (prod A B) A (@fst A B) nms)) *)
        destruct a.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
        apply snd_eq_not_in_map with (m := b); auto.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      * apply IHnms; auto.
  Qed.

  Lemma in_fold_left_by_cons_in :
    forall (l : list B) (g : B -> A) x acc,
      In x (fold_left (fun a b => g b :: a) l acc) ->
      In x acc \/ exists y, In y l /\ x = g y.
  Proof using A_eq_dec.
(* Goal: forall (l : list B) (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) l acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y l) (@eq A x (g y)))) *)
    intros until l.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) l acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y l) (@eq A x (g y)))) *)
    induction l.
    - auto.
    - simpl; intros.
(* Goal: and (@eq (list A) (@cons A a l) (@app A (@cons A a l1) l2)) (and (@eq (list B) (@map A B f (@cons A a l1)) (@cons B (f a) xs)) (@eq (list B) (@map A B f l2) ys)) *)
      destruct (A_eq_dec x (g a)); subst.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      + right; exists a; tauto.
      + find_apply_lem_hyp IHl.
(* Goal: or (@In A x acc) (@ex B (fun y : B => and (or (@eq B a y) (@In B y l)) (@eq A x (g y)))) *)
        break_or_hyp; [left|right].
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
        * find_apply_lem_hyp In_cons_neq; tauto.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
        * break_exists_exists; tauto.
  Qed.

  Lemma fold_left_for_each_not_in :
    forall (f : A -> B -> A) (g : A -> B -> C),
      (forall a b b',
          b <> b' ->
          g (f a b') b = g a b) ->
      forall l a b,
        ~ In b l ->
        g (fold_left f l a) b = g a b.
  Proof using A B C.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    induction l as [| b' l']; simpl in *; auto.
    - intros. intuition.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
      rewrite IHl'; auto.
  Qed.

  Lemma fold_left_for_each_in :
    forall (f : A -> B -> A) (g : A -> B -> C) (B_eq_dec : forall x y : B, {x = y} + {x <> y}),
      (forall a b b',
          b <> b' ->
          g (f a b') b = g a b) ->
      forall l a b,
        In b l ->
        exists a',
          g (fold_left f l a) b = g (f a' b) b.
  Proof using A B C.
(* Goal: and (@eq (list A) (@cons A a l) (@app A (@cons A a l1) l2)) (and (@eq (list B) (@map A B f (@cons A a l1)) (@cons B (f a) xs)) (@eq (list B) (@map A B f l2) ys)) *)
    induction l as [|b' l']; simpl in *; intuition; subst.
(* Goal: @eq C (g (@fold_left A B f l' (f a b')) b) (g a b) *)
    destruct (in_dec B_eq_dec b l'); intuition.
(* Goal: forall (g : forall _ : B, A) (x : A) (acc : list A) (_ : @In A x (@fold_left (list A) B (fun (a : list A) (b : B) => @cons A (g b) a) (@nil B) acc)), or (@In A x acc) (@ex B (fun y : B => and (@In B y (@nil B)) (@eq A x (g y)))) *)
    find_eapply_lem_hyp fold_left_for_each_not_in; eauto.
  Qed.

  Lemma hd_error_tl_exists :
    forall (l : list A) x,
      hd_error l = Some x ->
      exists tl,
        l = x :: tl.
  Proof.
(* Goal: forall (l : list A) (x : A) (_ : @eq (option A) (@hd_error A l) (@Some A x)), @ex (list A) (fun tl : list A => @eq (list A) l (@cons A x tl)) *)
    intros.
(* Goal: @eq (prod A B) (@pair A B a b) (@pair A B (@fst A B (@pair A B a b)) m) *)
    destruct l; simpl in *.
    - congruence.
    - eexists; solve_by_inversion.
  Qed.

  Lemma hd_error_None :
    forall (l : list A),
      hd_error l = None ->
      l = [].
  Proof.
(* Goal: forall (l : list A) (_ : @eq (option A) (@hd_error A l) (@None A)), @eq (list A) l (@nil A) *)
    now destruct l.
  Qed.

End list_util.

(* We have to repeat these Hint Resolve commands because hints don't survive
   past the ends of sections *)
Hint Resolve app_cons_in : struct_util.
Hint Resolve app_cons_in_rest : struct_util.
Hint Resolve in_rest_app_cons : struct_util.
