(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega Permutation.

Require Import list_focus utils_tac.

Set Implicit Arguments.

Create HintDb length_db.

Tactic Notation "rew" "length" := autorewrite with length_db.
Tactic Notation "rew" "length" "in" hyp(H) := autorewrite with length_db in H.

Infix "~p" := (@Permutation _) (at level 70).

Section length.
   
  Variable X : Type.

  Implicit Type l : list X.

  Fact length_nil : length (@nil X) = 0.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  Proof. auto. Qed.

  Fact length_cons x l : length (x::l) = S (length l).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  Proof. auto. Qed.

End length.

Hint Rewrite length_nil length_cons app_length map_length rev_length : length_db.

Section list_an.

  Fixpoint list_an a n :=
    match n with 
      | 0   => nil
      | S n => a::list_an (S a) n
    end.

  Fact list_an_S a n : list_an a (S n) = a::list_an (S a) n.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  Proof. auto. Qed. 

  Fact list_an_plus a n m : list_an a (n+m) = list_an a n ++ list_an (n+a) m.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    revert a; induction n; intros a; simpl; auto.
(* Goal: @eq (list nat) (@cons nat a (list_an (S a) (Init.Nat.add n m))) (@cons nat a (@app nat (list_an (S a) n) (list_an (S (Init.Nat.add n a)) m))) *)
    rewrite IHn; do 3 f_equal; omega.
  Qed.

  Fact list_an_length a n : length (list_an a n) = n.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    revert a; induction n; intro; simpl; f_equal; auto.
  Qed.
  
  Fact list_an_spec a n m : In m (list_an a n) <-> a <= m < a+n.
  Proof.
(* Goal: iff (@In nat m (list_an a n)) (and (le a m) (lt m (Init.Nat.add a n))) *)
    revert a; induction n as [ | n IHn ]; simpl; intros a; [ | rewrite IHn ]; omega. 
  Qed.

  Fact map_S_list_an a n : map S (list_an a n) = list_an (S a) n.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  Proof. revert a; induction n; simpl; intro; f_equal; auto. Qed.

  Fact list_an_app_inv a n l r : list_an a n = l++r -> l = list_an a (length l) /\ r = list_an (a+length l) (length r).
  Proof.
(* Goal: forall _ : @eq (list nat) (list_an a n) (@app nat l r), and (@eq (list nat) l (list_an a (@length nat l))) (@eq (list nat) r (list_an (Init.Nat.add a (@length nat l)) (@length nat r))) *)
    revert a l r; induction n as [ | n IHn ]; intros a l r; simpl.
    + destruct l; destruct r; intros; auto; discriminate.
    + destruct l as [ | x l ]; simpl; intros H1.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
      * split; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
        rewrite <- H1; simpl; rewrite Nat.add_0_r, list_an_length; auto.
      * injection H1; clear H1; intros H1 H0.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
        apply IHn in H1; destruct H1; split; f_equal; auto.
(* Goal: @eq (list nat) r (list_an (Init.Nat.add a (S (@length nat l))) (@length nat r)) *)
        rewrite H1 at 1; f_equal; omega.
  Qed.

End list_an.

Hint Rewrite list_an_length : length_db.

Definition list_fun_inv X (l : list X) (x : X) : { f : nat -> X | l = map f (list_an 0 (length l)) }.
Proof.
(* Goal: @sig (forall _ : nat, X) (fun f : forall _ : nat, X => @eq (list X) l (@map nat X f (list_an O (@length X l)))) *)
  induction l as [ | y l IHl ].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + exists (fun _ => x); auto.
  + destruct IHl as (f & Hf).
(* Goal: @sig (forall _ : nat, X) (fun f : forall _ : nat, X => @eq (list X) (@cons X y l) (@map nat X f (list_an O (@length X (@cons X y l))))) *)
    exists (fun i => match i with 0 => y | S i => f i end); simpl.
(* Goal: @eq (list X) (@cons X y l) (@cons X y (@map nat X (fun i : nat => match i with | O => y | S i0 => f i0 end) (list_an (S O) (@length X l)))) *)
    f_equal.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    rewrite Hf, <- map_S_list_an, map_length, list_an_length, map_map; auto.
Qed.

Fact list_upper_bound (l : list nat) : { m | forall x, In x l -> x < m }.
Proof.
(* Goal: @sig nat (fun m : nat => forall (x : nat) (_ : @In nat x l), lt x m) *)
  induction l as [ | x l (m & Hm) ].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + exists 0; simpl; tauto.
  + exists (1+x+m); intros y [ [] | H ]; simpl; try omega.
(* Goal: lt y (S (Init.Nat.add x m)) *)
    generalize (Hm _ H); intros; omega.
Qed.

Section list_injective.

  Variable X : Type.
   
  Definition list_injective (ll : list X) :=  forall l a m b r, ll = l ++ a :: m ++ b :: r -> a <> b.
  
  Fact in_list_injective_0 : list_injective nil.
  Proof. intros [] ? ? ? ? ?; discriminate. Qed.
  
  Fact in_list_injective_1 x ll : ~ In x ll -> list_injective ll -> list_injective (x::ll).
  Proof.
(* Goal: forall (_ : not (@In X x ll)) (_ : list_injective ll), list_injective (@cons X x ll) *)
    intros H1 H2 l a m b r H3.
(* Goal: not (@eq X a b) *)
    destruct l as [ | u l ].
(* Goal: not (@eq X a b) *)
    inversion H3; subst.
(* Goal: not (@eq X a b) *)
(* Goal: not (@eq X a b) *)
    destruct m as [ | v m ].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    contradict H1; subst; simpl; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    contradict H1; subst; simpl; right; apply in_or_app; right; left; auto.
(* Goal: not (@eq X a b) *)
    inversion H3; subst.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    apply (H2 l _ m _ r); auto.
  Qed.
  
  Fact list_injective_inv x ll : list_injective (x::ll) -> ~ In x ll /\ list_injective ll.
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
    split.
(* Goal: not (@In X x ll) *)
(* Goal: list_injective ll *)
    intros H1; apply in_split in H1; destruct H1 as (l & r & ?); subst.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    apply (H nil x l x r); auto.
(* Goal: list_injective ll *)
    intros l a m b r ?; apply (H (x::l) a m b r); subst; solve list eq.
  Qed.
  
  Variable P : list X -> Type.
  
  Hypothesis (HP0 : P nil).
  Hypothesis (HP1 : forall x l, ~ In x l -> P l -> P (x::l)).
  
  Theorem list_injective_rect l : list_injective l -> P l.
  Proof.
(* Goal: forall _ : list_injective l, P l *)
    induction l as [ [ | x l ] IHl ] using (measure_rect (@length _)).
(* Goal: forall _ : list_injective (@nil X), P (@nil X) *)
(* Goal: forall _ : list_injective (@cons X x l), P (@cons X x l) *)
    intro; apply HP0.
(* Goal: forall _ : list_injective (@cons X x l), P (@cons X x l) *)
    intros; apply HP1.
(* Goal: not (@In X x l) *)
(* Goal: P l *)
    apply list_injective_inv, H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    apply IHl; simpl; auto.
(* Goal: list_injective l *)
    apply list_injective_inv with (1 := H).
  Qed.

End list_injective.

Fact list_injective_map X Y (f : X -> Y) ll :
       (forall x y, f x = f y -> x = y) -> list_injective ll -> list_injective (map f ll).
Proof.
(* Goal: forall (_ : forall (x y : X) (_ : @eq Y (f x) (f y)), @eq X x y) (_ : @list_injective X ll), @list_injective Y (@map X Y f ll) *)
  intros Hf.
(* Goal: forall _ : @list_injective X ll, @list_injective Y (@map X Y f ll) *)
  induction 1 as [ | x l Hl IHl ] using list_injective_rect.
(* Goal: @list_injective Y (@map X Y f (@nil X)) *)
(* Goal: @list_injective Y (@map X Y f (@cons X x l)) *)
  apply in_list_injective_0.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  simpl; apply in_list_injective_1; auto.
(* Goal: not (@In Y (f x) (@map X Y f l)) *)
  contradict Hl.
(* Goal: @In X x l *)
  apply in_map_iff in Hl.
(* Goal: @In X x l *)
  destruct Hl as (y & Hl & ?).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  apply Hf in Hl; subst; auto.
Qed.

Section iter.
  
  Variable (X : Type) (f : X -> X).

  Fixpoint iter x n :=
    match n with
      | 0   => x
      | S n => iter (f x) n
    end.

  Fact iter_plus x a b : iter x (a+b) = iter (iter x a) b.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  Proof. revert x; induction a; intros x; simpl; auto. Qed.

  Fact iter_swap x n : iter (f x) n = f (iter x n).
  Proof. 
    change (iter (f x) n) with (iter x (1+n)).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    rewrite plus_comm, iter_plus; auto.
  Qed.

End iter.

Fixpoint list_repeat X (x : X) n :=
  match n with
    | 0   => nil
    | S n => x::list_repeat x n
  end.
  
Fact list_repeat_plus X x a b : @list_repeat X x (a+b) = list_repeat x a ++ list_repeat x b.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. induction a; simpl; f_equal; auto. Qed.
  
Fact list_repeat_length X x n : length (@list_repeat X x n) = n.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. induction n; simpl; f_equal; auto. Qed.

Fact In_list_repeat X (x y : X) n : In y (list_repeat x n) -> x = y /\ 0 < n.
Proof.
(* Goal: forall _ : @In X y (@list_repeat X x n), and (@eq X x y) (lt O n) *)
  induction n; simpl; intros [].
(* Goal: and (@eq X x y) (lt O (S n)) *)
(* Goal: and (@eq X x y) (lt O (S n)) *)
  split; auto; omega.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  split; try omega; apply IHn; auto.
Qed.

Fact map_list_repeat X Y f x n : @map X Y f (list_repeat x n) = list_repeat (f x) n.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. induction n; simpl; f_equal; auto. Qed.

Fact map_cst_repeat X Y (y : Y) ll : map (fun _ : X => y) ll = list_repeat y (length ll).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. induction ll; simpl; f_equal; auto. Qed.
  
Fact map_cst_snoc X Y (y : Y) ll mm : y :: map (fun _ : X => y) ll++mm = map (fun _ => y) ll ++ y::mm.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. induction ll; simpl; f_equal; auto. Qed.

Fact map_cst_rev  X Y (y : Y) ll : map (fun _ : X => y) (rev ll) = map (fun _ => y) ll.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. do 2 rewrite map_cst_repeat; rewrite rev_length; auto. Qed.

Fact In_perm X (x : X) l : In x l -> exists m, x::m ~p l.
Proof.
(* Goal: forall _ : @In X x l, @ex (list X) (fun m : list X => @Permutation X (@cons X x m) l) *)
  intros H; apply in_split in H.
(* Goal: @ex (list X) (fun m : list X => @Permutation X (@cons X x m) l) *)
  destruct H as (m & k & ?); subst.
  exists (m++k).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  apply Permutation_cons_app; auto.
Qed.

Fact list_app_eq_inv X (l1 l2 r1 r2 : list X) :
       l1++r1 = l2++r2 -> { m | l1++m = l2 /\ r1 = m++r2 } 
                        + { m | l2++m = l1 /\ r2 = m++r1 }.
Proof.
(* Goal: forall _ : @prefix X (@app X l1 l2) (@app X r1 r2), sumbool (@prefix X l1 r1) (@prefix X r1 l1) *)
  revert l2 r1 r2; induction l1 as [ | x l1 IH ].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  intros; left; exists l2; auto.
(* Goal: forall (l2 r1 r2 : list X) (_ : @eq (list X) (@app X (@cons X x l1) r1) (@app X l2 r2)), sum (@sig (list X) (fun m : list X => and (@eq (list X) (@app X (@cons X x l1) m) l2) (@eq (list X) r1 (@app X m r2)))) (@sig (list X) (fun m : list X => and (@eq (list X) (@app X l2 m) (@cons X x l1)) (@eq (list X) r2 (@app X m r1)))) *)
  intros [ | y l2 ] r1 r2; simpl; intros H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  right; exists (x::l1); auto.
(* Goal: sum (@sig (list X) (fun m : list X => and (@eq (list X) (@cons X x (@app X l1 m)) (@cons X y l2)) (@eq (list X) r1 (@app X m r2)))) (@sig (list X) (fun m : list X => and (@eq (list X) (@cons X y (@app X l2 m)) (@cons X x l1)) (@eq (list X) r2 (@app X m r1)))) *)
  inversion H.
  destruct (IH l2 r1 r2) as [ (m & Hm) | (m & Hm) ]; auto; 
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    [ left | right ]; exists m; split; f_equal; tauto.
Qed.

Fact list_app_cons_eq_inv X (l1 l2 r1 r2 : list X) x :
       l1++r1 = l2++x::r2 -> { m | l1++m = l2 /\ r1 = m++x::r2 } 
                           + { m | l2++x::m = l1 /\ r2 = m++r1 }.
Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  intros H.
(* Goal: and (@eq (list X) l1 l2) (and (@eq X x1 x2) (@eq (list X) r1 r2)) *)
  apply list_app_eq_inv in H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  destruct H as [ H | (m & H1 & H2) ]; auto.
(* Goal: @sigT (list Y) (fun m1 : list Y => @sig (list Y) (fun m2 : list Y => and (@Forall2 X Y R (@cons X x l1) m1) (and (@Forall2 X Y R l2 m2) (@eq (list Y) m (@app Y m1 m2))))) *)
  destruct m as [ | y m ].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  left; exists nil; simpl in *; split; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  revert H1; do 2 rewrite <- app_nil_end; auto.
(* Goal: sum (@sig (list X) (fun m : list X => and (@eq (list X) (@app X l1 m) l2) (@eq (list X) r1 (@app X m (@cons X x r2))))) (@sig (list X) (fun m : list X => and (@eq (list X) (@app X l2 (@cons X x m)) l1) (@eq (list X) r2 (@app X m r1)))) *)
  inversion H2; subst.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  right; exists m; auto.
Qed.

Fact list_cons_app_cons_eq_inv X (l2 r1 r2 : list X) x y :
       x::r1 = l2++y::r2 -> (l2 = nil /\ x = y /\ r1 = r2) 
                          + { m | l2 = x::m /\ r1 = m++y::r2 }.
Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  intros H.
(* Goal: sum (and (@eq (list X) l2 (@nil X)) (and (@eq X x y) (@eq (list X) r1 r2))) (@sig (list X) (fun m : list X => and (@eq (list X) l2 (@cons X x m)) (@eq (list X) r1 (@app X m (@cons X y r2))))) *)
  destruct l2 as [ | z m ]; simpl in H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + left; inversion H; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + right; exists m; inversion H; auto.
Qed.
 
Fact list_app_inj X (l1 l2 r1 r2 : list X) : length l1 = length l2 -> l1++r1 = l2++r2 -> l1 = l2 /\ r1 = r2.
Proof.
(* Goal: forall (_ : @eq nat (@length X l1) (@length X l2)) (_ : @eq (list X) (@app X l1 r1) (@app X l2 r2)), and (@eq (list X) l1 l2) (@eq (list X) r1 r2) *)
  revert l2; induction l1 as [ | x l1 IH ]; intros [ | y l2 ]; try discriminate.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  simpl; auto.
(* Goal: forall (_ : @eq nat (@length X (@cons X x l1)) (@length X (@cons X y l2))) (_ : @eq (list X) (@app X (@cons X x l1) r1) (@app X (@cons X y l2) r2)), and (@eq (list X) (@cons X x l1) (@cons X y l2)) (@eq (list X) r1 r2) *)
  intros H1 H2; inversion H1; inversion H2.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  apply IH in H4; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  split; f_equal; tauto.
Qed.

Fact list_split_length X (ll : list X) k : k <= length ll -> { l : _ & { r | ll = l++r /\ length l = k } }.
Proof.
(* Goal: forall _ : lt k (@length X ll), @sigT X (fun x : X => @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (@eq nat (@length X l) k)))) *)
  revert k; induction ll as [ | x ll IHll ]; intros k.
  exists nil, nil; split; simpl in * |- *; auto; omega.
(* Goal: forall _ : le k (@length X (@cons X x ll)), @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@cons X x ll) (@app X l r)) (@eq nat (@length X l) k))) *)
  destruct k as [ | k ]; intros Hk.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists nil, (x::ll); simpl; split; auto.
(* Goal: @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@cons X x ll) (@app X l r)) (@eq nat (@length X l) (S k)))) *)
  destruct (IHll k) as (l & r & H1 & H2).
(* Goal: le k (@length X ll) *)
(* Goal: @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@cons X x ll) (@app X l r)) (@eq nat (@length X l) (S k)))) *)
  simpl in Hk; omega.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists (x::l), r; split; simpl; auto; f_equal; auto.
Qed.

Fact list_pick X (ll : list X) k : k < length ll -> { x : _ & { l : _ & { r | ll = l++x::r /\ length l = k } } }.
Proof.
(* Goal: forall _ : lt k (@length X ll), @sigT X (fun x : X => @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (@eq nat (@length X l) k)))) *)
  revert k; induction ll as [ | x ll IHll ]; intros k.
(* Goal: forall _ : lt k (@length X (@nil X)), @sigT X (fun x : X => @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@nil X) (@app X l (@cons X x r))) (@eq nat (@length X l) k)))) *)
(* Goal: forall _ : lt k (@length X (@cons X x ll)), @sigT X (fun x0 : X => @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@cons X x ll) (@app X l (@cons X x0 r))) (@eq nat (@length X l) k)))) *)
  simpl; omega.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  destruct k as [ | k ]; intros H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists x, nil, ll; simpl; auto.
(* Goal: @ex (list X) (fun l1 : list X => @ex (list Y) (fun m1 : list Y => @ex X (fun x0 : X => @ex (list Y) (fun m2 : list Y => @ex (list X) (fun l2 : list X => and (@eq (list X) (@cons X x l) (@app X l1 (@cons X x0 l2))) (and (@eq (list Y) (f x0) (@app Y m1 (@cons Y y m2))) (and (@eq (list Y) r1 (@app Y (@flat_map X Y f l1) m1)) (@eq (list Y) r2 (@app Y m2 (@flat_map X Y f l2)))))))))) *)
  simpl in H.
(* Goal: @sigT X (fun x0 : X => @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@cons X x ll) (@app X l (@cons X x0 r))) (@eq nat (@length X l) (S k))))) *)
  destruct IHll with (k := k) as (y & l & r & ? & ?); try omega.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists y, (x::l), r; subst; simpl; split; auto.
Qed.

Fact list_split_middle X l1 (x1 : X) r1 l2 x2 r2 : 
       ~ In x1 l2 -> ~ In x2 l1 -> l1++x1::r1 = l2++x2::r2 -> l1 = l2 /\ x1 = x2 /\ r1 = r2.
Proof.
(* Goal: forall (_ : not (@In X x1 l2)) (_ : not (@In X x2 l1)) (_ : @eq (list X) (@app X l1 (@cons X x1 r1)) (@app X l2 (@cons X x2 r2))), and (@eq (list X) l1 l2) (and (@eq X x1 x2) (@eq (list X) r1 r2)) *)
  intros H1 H2 H.
(* Goal: and (@eq (list X) l1 l2) (and (@eq X x1 x2) (@eq (list X) r1 r2)) *)
  apply list_app_eq_inv in H.
(* Goal: and (@eq (list X) l1 l2) (and (@eq X x1 x2) (@eq (list X) r1 r2)) *)
  destruct H as [ (m & H3 & H4) | (m & H3 & H4) ]; destruct m.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  inversion H4; subst; rewrite <- app_nil_end; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  inversion H4; subst; destruct H1; apply in_or_app; right; left; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  inversion H4; subst; rewrite <- app_nil_end; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  inversion H4; subst; destruct H2; apply in_or_app; right; left; auto.
Qed.

Section flat_map.

  Variable (X Y : Type) (f : X -> list Y).

  Fact flat_map_app l1 l2 : flat_map f (l1++l2) = flat_map f l1 ++ flat_map f l2.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    induction l1; simpl; auto; solve list eq; f_equal; auto.
  Qed.

  Fact flat_map_app_inv l r1 y r2 : flat_map f l = r1++y::r2 -> exists l1 m1 x m2 l2, l = l1++x::l2 /\ f x = m1++y::m2 
                                                                  /\ r1 = flat_map f l1++m1 /\ r2 = m2++flat_map f l2. 
  Proof.
(* Goal: forall _ : @eq (list Y) (@flat_map X Y f l) (@app Y r1 (@cons Y y r2)), @ex (list X) (fun l1 : list X => @ex (list Y) (fun m1 : list Y => @ex X (fun x : X => @ex (list Y) (fun m2 : list Y => @ex (list X) (fun l2 : list X => and (@eq (list X) l (@app X l1 (@cons X x l2))) (and (@eq (list Y) (f x) (@app Y m1 (@cons Y y m2))) (and (@eq (list Y) r1 (@app Y (@flat_map X Y f l1) m1)) (@eq (list Y) r2 (@app Y m2 (@flat_map X Y f l2)))))))))) *)
    revert r1 y r2.
(* Goal: forall (r1 : list Y) (y : Y) (r2 : list Y) (_ : @eq (list Y) (@flat_map X Y f l) (@app Y r1 (@cons Y y r2))), @ex (list X) (fun l1 : list X => @ex (list Y) (fun m1 : list Y => @ex X (fun x : X => @ex (list Y) (fun m2 : list Y => @ex (list X) (fun l2 : list X => and (@eq (list X) l (@app X l1 (@cons X x l2))) (and (@eq (list Y) (f x) (@app Y m1 (@cons Y y m2))) (and (@eq (list Y) r1 (@app Y (@flat_map X Y f l1) m1)) (@eq (list Y) r2 (@app Y m2 (@flat_map X Y f l2)))))))))) *)
    induction l as [ | x l IHl ]; intros r1 y r2 H.
    + destruct r1; discriminate.
    + simpl in H.
(* Goal: @ex (list X) (fun l1 : list X => @ex (list Y) (fun m1 : list Y => @ex X (fun x0 : X => @ex (list Y) (fun m2 : list Y => @ex (list X) (fun l2 : list X => and (@eq (list X) (@cons X x l) (@app X l1 (@cons X x0 l2))) (and (@eq (list Y) (f x0) (@app Y m1 (@cons Y y m2))) (and (@eq (list Y) r1 (@app Y (@flat_map X Y f l1) m1)) (@eq (list Y) r2 (@app Y m2 (@flat_map X Y f l2)))))))))) *)
      apply list_app_cons_eq_inv in H.
(* Goal: @ex (list X) (fun l1 : list X => @ex (list Y) (fun m1 : list Y => @ex X (fun x0 : X => @ex (list Y) (fun m2 : list Y => @ex (list X) (fun l2 : list X => and (@eq (list X) (@cons X x l) (@app X l1 (@cons X x0 l2))) (and (@eq (list Y) (f x0) (@app Y m1 (@cons Y y m2))) (and (@eq (list Y) r1 (@app Y (@flat_map X Y f l1) m1)) (@eq (list Y) r2 (@app Y m2 (@flat_map X Y f l2)))))))))) *)
      destruct H as [ (m & Hm1 & Hm2) | (m & Hm1 & Hm2) ].
      - apply IHl in Hm2.
(* Goal: @ex (list X) (fun l1 : list X => @ex (list Y) (fun m1 : list Y => @ex X (fun x0 : X => @ex (list Y) (fun m2 : list Y => @ex (list X) (fun l2 : list X => and (@eq (list X) (@cons X x l) (@app X l1 (@cons X x0 l2))) (and (@eq (list Y) (f x0) (@app Y m1 (@cons Y y m2))) (and (@eq (list Y) r1 (@app Y (@flat_map X Y f l1) m1)) (@eq (list Y) r2 (@app Y m2 (@flat_map X Y f l2)))))))))) *)
        destruct Hm2 as (l1 & m1 & x' & m2 & l2 & G1 & G2 & G3 & G4); subst.
(* Goal: @ex (list X) (fun l3 : list X => @ex (list Y) (fun m3 : list Y => @ex X (fun x0 : X => @ex (list Y) (fun m4 : list Y => @ex (list X) (fun l4 : list X => and (@eq (list X) (@cons X x (@app X l1 (@cons X x' l2))) (@app X l3 (@cons X x0 l4))) (and (@eq (list Y) (f x0) (@app Y m3 (@cons Y y m4))) (and (@eq (list Y) (@app Y (f x) (@app Y (@flat_map X Y f l1) m1)) (@app Y (@flat_map X Y f l3) m3)) (@eq (list Y) (@app Y m2 (@flat_map X Y f l2)) (@app Y m4 (@flat_map X Y f l4)))))))))) *)
        exists (x::l1), m1, x', m2, l2; simpl; repeat (split; auto).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
        rewrite app_ass; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
      - exists nil, r1, x, m, l; auto.
  Qed.

End flat_map.

Definition prefix X (l ll : list X) := exists r, ll = l++r.
  
Infix "<p" := (@prefix _) (at level 70, no associativity).
  
Section prefix. (* as an inductive predicate *)
   
  Variable X : Type.
  
  Implicit Types (l ll : list X).
  
  Fact in_prefix_0 ll : nil <p ll.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    exists ll; auto.
  Qed.
  
  Fact in_prefix_1 x l ll : l <p ll -> x::l <p x::ll.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    intros (r & ?); subst; exists r; auto.
  Qed.

  Fact prefix_length l m : l <p m -> length l <= length m.
  Proof. intros (? & ?); subst; rew length; omega. Qed.
  
  Fact prefix_app_lft l r1 r2 : r1 <p r2 -> l++r1 <p l++r2.
  Proof.
(* Goal: forall _ : @prefix X r1 r2, @prefix X (@app X l r1) (@app X l r2) *)
    intros (a & ?); subst.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    exists a; rewrite app_ass; auto.
  Qed.
  
  Fact prefix_inv x y l ll : x::l <p y::ll -> x = y /\ l <p ll.
  Proof.
(* Goal: forall _ : @prefix X (@cons X x l) (@cons X y ll), and (@eq X x y) (@prefix X l ll) *)
    intros (r & Hr).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    inversion Hr; split; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    exists r; auto.
  Qed.
  
  Fact prefix_list_inv l r rr : l++r <p l++rr -> r <p rr.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    induction l as [ | x l IHl ]; simpl; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    intros H; apply prefix_inv, proj2, IHl in H; auto.
  Qed.

  Fact prefix_refl l : l <p l.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  Proof. exists nil; rewrite <- app_nil_end; auto. Qed.

  Fact prefix_trans l1 l2 l3 : l1 <p l2 -> l2 <p l3 -> l1 <p l3.
  Proof. intros (m1 & H1) (m2 & H2); subst; exists (m1++m2); solve list eq. Qed.

  Section prefix_rect.

    Variables (P : list X -> list X -> Type)
              (HP0 : forall ll, P nil ll)
              (HP1 : forall x l ll, l <p ll -> P l ll -> P (x::l) (x::ll)).
              
    Definition prefix_rect l ll : prefix l ll -> P l ll.
    Proof.
(* Goal: forall _ : @prefix X l ll, P l ll *)
      revert l; induction ll as [ | x ll IHll ]; intros l H.
      
(* Goal: P l (@nil X) *)
(* Goal: P l (@cons X x ll) *)
      replace l with (nil : list X).
(* Goal: P (@nil X) (@cons X x ll) *)
(* Goal: P (@cons X y l) (@cons X x ll) *)
      apply HP0.
(* Goal: @eq (list X) (@nil X) l *)
(* Goal: P l (@cons X x ll) *)
      destruct H as (r & Hr).
(* Goal: @eq (list X) (@nil X) l *)
(* Goal: P l (@cons X x ll) *)
      destruct l; auto; discriminate.
      
(* Goal: @sigT Y (fun b : Y => @sig (list Y) (fun mm' : list Y => and (R a b) (and (@eq (list Y) mm (@cons Y b mm')) (@Forall2 X Y R ll mm')))) *)
      destruct l as [ | y l ].
(* Goal: P (@nil X) (@cons X x ll) *)
(* Goal: P (@cons X y l) (@cons X x ll) *)
      apply HP0.
(* Goal: P (@cons X y l) (@cons X x ll) *)
      apply prefix_inv in H.
(* Goal: P (@cons X y l) (@cons X x ll) *)
      destruct H as (? & E); subst y.
(* Goal: P (@cons X x l) (@cons X x ll) *)
      apply HP1; [ | apply IHll ]; trivial.
    Qed.
   
  End prefix_rect.

  Fact prefix_app_inv l1 l2 r1 r2 : l1++l2 <p r1++r2 -> { l1 <p r1 } + { r1 <p l1 }.
  Proof.
(* Goal: forall _ : @prefix X (@app X l1 l2) (@app X r1 r2), sumbool (@prefix X l1 r1) (@prefix X r1 l1) *)
    revert l2 r1 r2; induction l1 as [ | x l1 IH ].
(* Goal: forall (l2 r1 r2 : list X) (_ : @prefix X (@app X (@nil X) l2) (@app X r1 r2)), sumbool (@prefix X (@nil X) r1) (@prefix X r1 (@nil X)) *)
(* Goal: forall (l2 r1 r2 : list X) (_ : @prefix X (@app X (@cons X x l1) l2) (@app X r1 r2)), sumbool (@prefix X (@cons X x l1) r1) (@prefix X r1 (@cons X x l1)) *)
    left; apply in_prefix_0.
(* Goal: forall (l2 r1 r2 : list X) (_ : @prefix X (@app X (@cons X x l1) l2) (@app X r1 r2)), sumbool (@prefix X (@cons X x l1) r1) (@prefix X r1 (@cons X x l1)) *)
    intros l2 [ | y r1 ] r2.
(* Goal: forall _ : @prefix X (@app X (@cons X x l1) l2) (@app X (@nil X) r2), sumbool (@prefix X (@cons X x l1) (@nil X)) (@prefix X (@nil X) (@cons X x l1)) *)
(* Goal: forall _ : @prefix X (@app X (@cons X x l1) l2) (@app X (@cons X y r1) r2), sumbool (@prefix X (@cons X x l1) (@cons X y r1)) (@prefix X (@cons X y r1) (@cons X x l1)) *)
    right; apply in_prefix_0.
(* Goal: P (@cons X y l) (@cons X x ll) *)
    simpl; intros H; apply prefix_inv in H.
(* Goal: sumbool (@prefix X (@cons X x l1) (@cons X y r1)) (@prefix X (@cons X y r1) (@cons X x l1)) *)
    destruct H as (E & H); subst y.
    destruct IH with (1 := H); [ left | right ];
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
      apply in_prefix_1; auto.
  Qed. 
  
End prefix.

Definition prefix_spec X (l ll : list X) : l <p ll -> { r | ll = l ++ r }.
Proof.
(* Goal: forall _ : @prefix X l ll, @sig (list X) (fun r : list X => @eq (list X) ll (@app X l r)) *)
  induction 1 as [ ll | x l ll _ (r & Hr) ] using prefix_rect.
(* Goal: @sig (list X) (fun r : list X => @eq (list X) ll (@app X (@nil X) r)) *)
(* Goal: @sig (list X) (fun r : list X => @eq (list X) (@cons X x ll) (@app X (@cons X x l) r)) *)
  exists ll; trivial.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists r; simpl; f_equal; auto.
Qed.

Fact prefix_app_lft_inv X (l1 l2 m : list X) : l1++l2 <p m -> { m2 | m = l1++m2 /\ l2 <p m2 }.
Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  intros H.
(* Goal: @sig (list X) (fun m2 : list X => and (@eq (list X) m (@app X l1 m2)) (@prefix X l2 m2)) *)
  apply prefix_spec in H. 
(* Goal: @sig (list X) (fun m2 : list X => and (@eq (list X) m (@app X l1 m2)) (@prefix X l2 m2)) *)
  destruct H as (r & H).
  exists (l2++r); simpl.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  solve list eq in H; split; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists r; auto.
Qed.

Section list_assoc.

  Variables (X Y : Type) (eq_X_dec : eqdec X).

  Fixpoint list_assoc x l : option Y :=
    match l with 
      | nil  => None
      | (y,a)::l => if eq_X_dec x y then Some a else list_assoc x l
    end.

  Fact list_assoc_eq x y l x' : x = x' -> list_assoc x' ((x,y)::l) = Some y.
  Proof.    
(* Goal: forall _ : @eq X x x', @eq (option Y) (list_assoc x' (@cons (prod X Y) (@pair X Y x y) l)) (@Some Y y) *)
    intros []; simpl.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct (eq_X_dec x x) as [ | [] ]; auto.
  Qed.

  Fact list_assoc_neq x y l x' : x <> x' -> list_assoc x' ((x,y)::l) = list_assoc x' l.
  Proof.    
(* Goal: forall _ : not (@eq X x x'), @eq (option Y) (list_assoc x' (@cons (prod X Y) (@pair X Y x y) l)) (list_assoc x' l) *)
    intros H; simpl.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct (eq_X_dec x' x) as [ | ]; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct H; auto.
  Qed.

  Fact list_assoc_In x l : 
    match list_assoc x l with 
      | None   => ~ In x (map fst l)
      | Some y => In (x,y) l
    end.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    induction l as  [ | (x',y) l IHl ]; simpl; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct (eq_X_dec x x'); subst; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct (list_assoc x l); auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    intros [ ? | ]; subst; tauto.
  Qed.

  Fact In_list_assoc x l : In x (map fst l) -> { y | list_assoc x l = Some y /\ In (x,y) l }.
  Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
    intros H.
(* Goal: @eq (option Y) (list_assoc x l) (@None Y) *)
    generalize (list_assoc_In x l).
(* Goal: forall _ : match list_assoc x l with | Some y => @In (prod X Y) (@pair X Y x y) l | None => not (@In X x (@map (prod X Y) X (@fst X Y) l)) end, @sig Y (fun y : Y => and (@eq (option Y) (list_assoc x l) (@Some Y y)) (@In (prod X Y) (@pair X Y x y) l)) *)
    destruct (list_assoc x l) as [ y | ].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    exists y; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    tauto.
  Qed.
  
  Fact not_In_list_assoc x l : ~ In x (map fst l) -> list_assoc x l = None.
  Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
    intros H.
(* Goal: @eq (option Y) (list_assoc x l) (@None Y) *)
    generalize (list_assoc_In x l).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct (list_assoc x l) as [ y | ]; auto.
(* Goal: forall _ : @In (prod X Y) (@pair X Y x y) l, @eq (option Y) (@Some Y y) (@None Y) *)
    intros H1; contradict H.
(* Goal: @In X x (@map (prod X Y) X (@fst X Y) l) *)
    apply in_map_iff.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    exists (x,y); simpl; auto.
  Qed.

  Fact list_assoc_app x ll mm : list_assoc x (ll++mm) 
                              = match list_assoc x ll with
                                  | None   => list_assoc x mm
                                  | Some y => Some y
                                end.
  Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    induction ll as [ | (x',?) ]; simpl; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    destruct (eq_X_dec x x'); auto.
  Qed.

End list_assoc.

Section list_first_dec.

  Variable (X : Type) (P : X -> Prop) (Pdec : forall x, { P x } + { ~ P x }).
  
  Theorem list_choose_dec ll : { l : _ & { x : _ & { r | ll = l++x::r /\ P x /\ forall y, In y l -> ~ P y } } }
                             + { forall x, In x ll -> ~ P x }.
  Proof.
    induction ll as [ | a ll IH ];
      [ | destruct (Pdec a) as [ Ha | Ha ]; [ | destruct IH as [ (l & x & r & H1 & H2 & H3) | H ]] ].
    * right; intros _ [].
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    * left; exists nil, a, ll; repeat split; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    * left; exists (a::l), x, r; repeat split; subst; auto. 
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
      intros ? [ | ]; subst; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    * right; intros ? [ | ]; subst; auto.
  Qed.
  
  Theorem list_first_dec a ll : P a -> In a ll -> { l : _ & { x : _ & { r | ll = l++x::r /\ P x /\ forall y, In y l -> ~ P y } } }.
  Proof.
(* Goal: forall (_ : P a) (_ : @In X a ll), @sigT (list X) (fun l : list X => @sigT X (fun x : X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (and (P x) (forall (y : X) (_ : @In X y l), not (P y)))))) *)
    intros H1 H2.
(* Goal: @sigT (list X) (fun l : list X => @sigT X (fun x : X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (and (P x) (forall (y : X) (_ : @In X y l), not (P y)))))) *)
    destruct (list_choose_dec ll) as [ H | H ]; trivial.
(* Goal: @sigT (list X) (fun l : list X => @sigT X (fun x : X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (and (P x) (forall (y : X) (_ : @In X y l), not (P y)))))) *)
    destruct (H _ H2 H1).
  Qed.
  
End list_first_dec.

Section map.

  Variable (X Y : Type) (f : X -> Y).
  
  Fact map_cons_inv ll y m : map f ll = y::m -> { x : _ & { l | ll = x::l /\ f x = y /\ map f l = m } }.
  Proof.
(* Goal: forall _ : @eq (list Y) (@map X Y f ll) (@cons Y y m), @sigT X (fun x : X => @sig (list X) (fun l : list X => and (@eq (list X) ll (@cons X x l)) (and (@eq Y (f x) y) (@eq (list Y) (@map X Y f l) m)))) *)
    destruct ll as [ | x l ]; try discriminate; simpl.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    intros H; inversion H; subst; exists x, l; auto.
  Qed.

  Fact map_app_inv ll m n : map f ll = m++n -> { l : _  & { r | ll = l++r /\ m = map f l /\ n = map f r } }.
  Proof.
(* Goal: forall _ : @eq (list Y) (@map X Y f ll) (@app Y m n), @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l r)) (and (@eq (list Y) m (@map X Y f l)) (@eq (list Y) n (@map X Y f r))))) *)
    revert m n; induction ll as [ | x ll IH ]; intros m n H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    * destruct m; destruct n; try discriminate; exists nil, nil; auto.
    * destruct m as [ | y m ]; simpl in H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
      + exists nil, (x::ll); auto.
      + inversion H; subst y.
(* Goal: @sigT (list X) (fun l : list X => @sig (list X) (fun r : list X => and (@eq (list X) (@cons X x ll) (@app X l r)) (and (@eq (list Y) (@cons Y (f x) m) (@map X Y f l)) (@eq (list Y) n (@map X Y f r))))) *)
        destruct IH with (1 := H2) as (l & r & H3 & H4 & H5); subst.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
        exists (x::l), r; auto.
  Qed.
  
  Fact map_middle_inv ll m y n : map f ll = m++y::n -> { l : _ & { x : _ & { r | ll = l++x::r /\ map f l = m /\ f x = y /\ map f r = n } } }.
  Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
    intros H.
(* Goal: @sigT (list X) (fun l : list X => @sigT X (fun x : X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (and (@eq (list Y) (@map X Y f l) m) (and (@eq Y (f x) y) (@eq (list Y) (@map X Y f r) n)))))) *)
    destruct map_app_inv with (1 := H) as (l & r & H1 & H2 & H3).
(* Goal: @sigT (list X) (fun l : list X => @sigT X (fun x : X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (and (@eq (list Y) (@map X Y f l) m) (and (@eq Y (f x) y) (@eq (list Y) (@map X Y f r) n)))))) *)
    symmetry in H3.
(* Goal: @sigT (list X) (fun l : list X => @sigT X (fun x : X => @sig (list X) (fun r : list X => and (@eq (list X) ll (@app X l (@cons X x r))) (and (@eq (list Y) (@map X Y f l) m) (and (@eq Y (f x) y) (@eq (list Y) (@map X Y f r) n)))))) *)
    destruct map_cons_inv with (1 := H3) as (x & r' & H4 & H5 & H6); subst.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
    exists l, x, r'; auto.
  Qed.
  
End map.

Fact Forall2_mono X Y (R S : X -> Y -> Prop) :
         (forall x y, R x y -> S x y) -> forall l m, Forall2 R l m -> Forall2 S l m.
Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  induction 2; constructor; auto.
Qed. 

Fact Forall2_nil_inv_l X Y R m : @Forall2 X Y R nil m -> m = nil.
Proof.
(* Goal: forall _ : @Forall2 X Y R m (@nil Y), @eq (list X) m (@nil X) *)
  inversion_clear 1; reflexivity.
Qed.

Fact Forall2_nil_inv_r X Y R m : @Forall2 X Y R m nil -> m = nil.
Proof.
(* Goal: forall _ : @Forall2 X Y R m (@nil Y), @eq (list X) m (@nil X) *)
  inversion_clear 1; reflexivity.
Qed.

Fact Forall2_cons_inv X Y R x l y m : @Forall2 X Y R (x::l) (y::m) <-> R x y /\ Forall2 R l m.
Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  inversion_clear 1; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  intros []; constructor; auto.
Qed.

Fact Forall2_app_inv_l X Y R l1 l2 m : 
    @Forall2 X Y R (l1++l2) m -> { m1 : _ & { m2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ m = m1++m2 } }.
Proof.
  revert l2 m;
  induction l1 as [ | x l1 IH ]; simpl; intros l2 m H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists nil, m; repeat split; auto.
(* Goal: @sigT (list Y) (fun m1 : list Y => @sig (list Y) (fun m2 : list Y => and (@Forall2 X Y R (@cons X x l1) m1) (and (@Forall2 X Y R l2 m2) (@eq (list Y) m (@app Y m1 m2))))) *)
  destruct m as [ | y m ].
(* Goal: @sigT (list Y) (fun m1 : list Y => @sig (list Y) (fun m2 : list Y => and (@Forall2 X Y R (@cons X x l1) m1) (and (@Forall2 X Y R l2 m2) (@eq (list Y) (@nil Y) (@app Y m1 m2))))) *)
(* Goal: @sigT (list Y) (fun m1 : list Y => @sig (list Y) (fun m2 : list Y => and (@Forall2 X Y R (@cons X x l1) m1) (and (@Forall2 X Y R l2 m2) (@eq (list Y) (@cons Y y m) (@app Y m1 m2))))) *)
  apply Forall2_nil_inv_r in H; discriminate H.
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@cons X x l) (@app X l1 l2))))) *)
  apply Forall2_cons_inv in H; destruct H as [ H1 H2 ].
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@cons X x l) (@app X l1 l2))))) *)
  apply IH in H2.
(* Goal: @sigT (list Y) (fun m1 : list Y => @sig (list Y) (fun m2 : list Y => and (@Forall2 X Y R (@cons X x l1) m1) (and (@Forall2 X Y R l2 m2) (@eq (list Y) (@cons Y y m) (@app Y m1 m2))))) *)
  destruct H2 as (m1 & m2 & H2 & H3 & H4); subst m.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists (y::m1), m2; repeat split; auto.
Qed.

Fact Forall2_app_inv_r X Y R l m1 m2 : 
    @Forall2 X Y R l (m1++m2) -> { l1 : _ & { l2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ l = l1++l2 } }.
Proof.
  revert m2 l;
  induction m1 as [ | y m1 IH ]; simpl; intros m2 l H.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists nil, l; repeat split; auto.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  destruct l as [ | x l ].
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@nil X) (@app X l1 l2))))) *)
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@cons X x l) (@app X l1 l2))))) *)
  apply Forall2_nil_inv_l in H; discriminate H.
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@cons X x l) (@app X l1 l2))))) *)
  apply Forall2_cons_inv in H; destruct H as [ H1 H2 ].
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@cons X x l) (@app X l1 l2))))) *)
  apply IH in H2.
(* Goal: @sigT (list X) (fun l1 : list X => @sig (list X) (fun l2 : list X => and (@Forall2 X Y R l1 (@cons Y y m1)) (and (@Forall2 X Y R l2 m2) (@eq (list X) (@cons X x l) (@app X l1 l2))))) *)
  destruct H2 as (l1 & l2 & H2 & H3 & H4); subst l.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists (x::l1), l2; repeat split; auto.
Qed.

Fact Forall2_cons_inv_l X Y R a ll mm : 
      @Forall2 X Y R (a::ll) mm 
   -> { b : _ & { mm' | R a b /\ mm = b::mm' /\ Forall2 R ll mm' } }.
Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  intros H.
(* Goal: @sigT Y (fun b : Y => @sig (list Y) (fun mm' : list Y => and (R a b) (and (@eq (list Y) mm (@cons Y b mm')) (@Forall2 X Y R ll mm')))) *)
  apply Forall2_app_inv_l with (l1 := a::nil) (l2 := ll) in H.
(* Goal: @sigT Y (fun b : Y => @sig (list Y) (fun mm' : list Y => and (R a b) (and (@eq (list Y) mm (@cons Y b mm')) (@Forall2 X Y R ll mm')))) *)
  destruct H as (l & mm' & H1 & H2 & H3).
(* Goal: @sigT Y (fun b : Y => @sig (list Y) (fun mm' : list Y => and (R a b) (and (@eq (list Y) mm (@cons Y b mm')) (@Forall2 X Y R ll mm')))) *)
  destruct l as [ | y l ].
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  exfalso; inversion H1.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  apply Forall2_cons_inv in H1.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  destruct H1 as [ H1 H4 ].
(* Goal: @sigT Y (fun b : Y => @sig (list Y) (fun mm' : list Y => and (R a b) (and (@eq (list Y) mm (@cons Y b mm')) (@Forall2 X Y R ll mm')))) *)
  apply Forall2_nil_inv_l in H4; subst l.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists y, mm'; auto.
Qed.

Fact Forall2_cons_inv_r X Y R b ll mm : 
      @Forall2 X Y R ll (b::mm) 
   -> { a : _ & { ll' | R a b /\ ll = a::ll' /\ Forall2 R ll' mm } }.
Proof.
(* Goal: forall _ : @Forall2 X Y R ll (@cons Y b mm), @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  intros H.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  apply Forall2_app_inv_r with (m1 := b::nil) (m2 := mm) in H.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  destruct H as (l & ll' & H1 & H2 & H3).
  destruct l as [ | x l  ].
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  exfalso; inversion H1.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  apply Forall2_cons_inv in H1.
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  destruct H1 as [ H1 H4 ].
(* Goal: @sigT X (fun a : X => @sig (list X) (fun ll' : list X => and (R a b) (and (@eq (list X) ll (@cons X a ll')) (@Forall2 X Y R ll' mm)))) *)
  apply Forall2_nil_inv_r in H4; subst l.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  exists x, ll'; auto.
Qed.

Fact Forall2_map_left X Y Z (R : Y -> X -> Prop) (f : Z -> Y) ll mm : Forall2 R (map f ll) mm <-> Forall2 (fun x y => R (f x) y) ll mm.
Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: forall _ : @Forall2 Y X R mm (@map Z X f ll), @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll *)
(* Goal: forall _ : @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll, @Forall2 Y X R mm (@map Z X f ll) *)
  revert mm.
(* Goal: forall (mm : list Y) (_ : @Forall2 Y X R mm (@map Z X f ll)), @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll *)
(* Goal: forall _ : @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll, @Forall2 Y X R mm (@map Z X f ll) *)
  induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail).
(* Goal: @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) (@cons Y y mm) (@cons Z a ll) *)
(* Goal: forall _ : @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll, @Forall2 Y X R mm (@map Z X f ll) *)
  apply Forall2_cons_inv in H; constructor. 
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  tauto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  apply IHll; tauto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  induction 1; constructor; auto.
Qed.

Fact Forall2_map_right X Y Z (R : Y -> X -> Prop) (f : Z -> X) mm ll : Forall2 R mm (map f ll) <-> Forall2 (fun y x => R y (f x)) mm ll.
Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: forall _ : @Forall2 Y X R mm (@map Z X f ll), @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll *)
(* Goal: forall _ : @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll, @Forall2 Y X R mm (@map Z X f ll) *)
  revert mm.
(* Goal: forall (mm : list Y) (_ : @Forall2 Y X R mm (@map Z X f ll)), @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll *)
(* Goal: forall _ : @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll, @Forall2 Y X R mm (@map Z X f ll) *)
  induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail).
(* Goal: @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) (@cons Y y mm) (@cons Z a ll) *)
(* Goal: forall _ : @Forall2 Y Z (fun (y : Y) (x : Z) => R y (f x)) mm ll, @Forall2 Y X R mm (@map Z X f ll) *)
  apply Forall2_cons_inv in H; constructor. 
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  tauto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  apply IHll; tauto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  induction 1; constructor; auto.
Qed.

Fact Forall2_map_both X Y X' Y' (R : X -> Y -> Prop) (f : X' -> X) (g : Y' -> Y) ll mm : Forall2 R (map f ll) (map g mm) <-> Forall2 (fun x y => R (f x) (g y)) ll mm.
Proof.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  rewrite Forall2_map_left, Forall2_map_right; split; auto.
Qed.

Fact Forall2_Forall X (R : X -> X -> Prop) ll : Forall2 R ll ll <-> Forall (fun x => R x x) ll.
Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  induction ll as [ | x ll ]; inversion_clear 1; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  induction 1; auto.
Qed.

Fact Forall_app X (P : X -> Prop) ll mm : Forall P (ll++mm) <-> Forall P ll /\ Forall P mm.
Proof.
(* Goal: iff (@Forall X P (@app X ll mm)) (and (@Forall X P ll) (@Forall X P mm)) *)
  repeat rewrite Forall_forall.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: forall _ : forall (x : X) (_ : @In X x (@app X ll mm)), P x, and (forall (x : X) (_ : @In X x ll), P x) (forall (x : X) (_ : @In X x mm), P x) *)
(* Goal: forall (_ : and (forall (x : X) (_ : @In X x ll), P x) (forall (x : X) (_ : @In X x mm), P x)) (x : X) (_ : @In X x (@app X ll mm)), P x *)
  firstorder.
(* Goal: forall (_ : and (forall (x : X) (_ : @In X x ll), P x) (forall (x : X) (_ : @In X x mm), P x)) (x : X) (_ : @In X x (@app X ll mm)), P x *)
  intros (H1 & H2) x Hx.
(* Goal: forall _ : forall (x : X) (_ : @In X x (@app X ll mm)), P x, and (forall (x : X) (_ : @In X x ll), P x) (forall (x : X) (_ : @In X x mm), P x) *)
(* Goal: forall (_ : and (forall (x : X) (_ : @In X x ll), P x) (forall (x : X) (_ : @In X x mm), P x)) (x : X) (_ : @In X x (@app X ll mm)), P x *)
  apply in_app_or in Hx; firstorder.
Qed.

Fact Forall_cons_inv X (P : X -> Prop) x ll : Forall P (x::ll) <-> P x /\ Forall P ll.
Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + inversion 1; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + constructor; tauto.
Qed.

Fact Forall_rev X (P : X -> Prop) ll : Forall P ll -> Forall P (rev ll).
Proof.
(* Goal: forall _ : @Forall X P ll, @Forall X P (@rev X ll) *)
  induction 1 as [ | x ll Hll IH ].
(* Goal: @Forall X P (@rev X (@nil X)) *)
(* Goal: @Forall X P (@rev X (@cons X x ll)) *)
  constructor.
(* Goal: @Forall X P (@rev X (@cons X x ll)) *)
  simpl.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  apply Forall_app; split; auto.
Qed.

Fact Forall_map X Y (f : X -> Y) (P : Y -> Prop) ll : Forall P (map f ll) <-> Forall (fun x => P (f x)) ll.
Proof.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + induction ll; simpl; try rewrite Forall_cons_inv; constructor; tauto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + induction 1; simpl; constructor; auto.
Qed.

Fact Forall_forall_map X (f : nat -> X) n l (P : X -> Prop) :
           l = map f (list_an 0 n) -> (forall i, i < n -> P (f i)) <-> Forall P l.
Proof.
(* Goal: forall _ : @eq (list X) l (@map nat X f (list_an O n)), iff (forall (i : nat) (_ : lt i n), P (f i)) (@Forall X P l) *)
  intros Hl; rewrite Forall_forall.
(* Goal: iff (forall (i : nat) (_ : lt i n), P (f i)) (forall (x : X) (_ : @In X x l), P x) *)
  split.
  + intros H x; rewrite Hl, in_map_iff.
(* Goal: forall _ : @ex nat (fun x0 : nat => and (@eq X (f x0) x) (@In nat x0 (list_an O n))), P x *)
    intros (y & ? & H1).
(* Goal: P x *)
    apply list_an_spec in H1; subst; apply H; omega.
  + intros H x Hx; apply H; rewrite Hl, in_map_iff.
(* Goal: @ex nat (fun x0 : nat => and (@eq X (f x0) (f x)) (@In nat x0 (list_an O n))) *)
    exists x; split; auto; apply list_an_spec; omega.
Qed.

Fact Forall_impl X (P Q : X -> Prop) ll : (forall x, In x ll -> P x -> Q x) -> Forall P ll -> Forall Q ll.
Proof.
(* Goal: @Forall X P (@rev X (@nil X)) *)
(* Goal: @Forall X P (@rev X (@cons X x ll)) *)
  intros H; induction 1 as [ | x ll Hx Hll IH ]; constructor.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + apply H; simpl; auto.
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
  + apply IH; intros ? ?; apply H; simpl; auto.
Qed.

Fact Forall_filter X (P : X -> Prop) (f : X -> bool) ll : Forall P ll -> Forall P (filter f ll).
(* Goal: @eq (list nat) (list_an a (S n)) (@cons nat a (list_an (S a) n)) *)
Proof. induction 1; simpl; auto; destruct (f x); auto. Qed.


