(* Copyright (C) 2005-2008 Sebastien Briais *)
(* http://lamp.epfl.ch/~sbriais/ *)

(* This library is free software; you can redistribute it and/or modify *)
(* it under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation; either version 2.1 of the *)
(* License, or (at your option) any later version. *)

(* This library is distributed in the hope that it will be useful, but *)
(* WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *)
(* Lesser General Public License for more details. *)

(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)

Require Import Wf_nat.
Require Import missing.
Require Export List Permutation.

(** we define some notions on lists such as being a permutation of *)

(** insertion x l l' iff l' is l where x has been inserted somewhere *)
Inductive insertion (A:Set) : A -> list A -> list A -> Prop :=
  head_insertion : forall (x:A)(l:list A),(insertion A x l (x::l))
|tail_insertion : forall (x y:A)(l l':list A),(insertion A x l l')->(insertion A x (y::l) (y::l')).

Lemma insertion_snoc : forall (A:Set)(x:A)(xs:list A),(insertion _ x xs (app xs (cons x nil))).
(* Goal: forall (A : Set) (x : A) (xs : list A), insertion A x xs (@app A xs (@cons A x (@nil A))) *)
  induction xs.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  apply head_insertion.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: insertion A x0 (@cons A a xs) (@cons A a xss) *)
  apply tail_insertion.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
Qed.

(** if (insertion x l l') then x is in l' *)
Lemma insertion_in : forall (A:Set)(x:A)(l l':list A),(insertion A x l l')->(In x l').
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  induction H;simpl;tauto.
Qed.

(** if (insertion x l l') then l is included in l' *)
Lemma insertion_inclusion : forall (A:Set)(x:A)(l l':list A),(insertion A x l l')->forall (y:A),(In y l)->(In y l').
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction l;simpl;try tauto;intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  inversion H;simpl;try tauto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  case H0;try tauto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  right;auto.
Qed.

(** if x is in l, then there is l' such that (insertion x l' l) *)
Lemma in_insertion : forall (A:Set)(x:A)(l:list A),(In x l)->exists l':list A,(insertion A x l' l).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction l;simpl;try tauto;intros.
(* Goal: @ex (list A) (fun l' : list A => insertion A x l' (@cons A a l)) *)
  case H;intro.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  rewrite H0;exists l;apply head_insertion.
(* Goal: @ex (list A) (fun l' : list A => insertion A x l' (@cons A a l)) *)
  elim (IHl H0);intro l';intro.
(* Goal: @ex (list A) (fun l' : list A => insertion A x l' (@cons A a l)) *)
  exists (a::l');apply tail_insertion;trivial.
Qed.

(** if (insertion x l l') and y is in l' then y=x or y is in l *)
Lemma in_insertion_inv : forall (A:Set)(x y:A)(l l':list A),(insertion A y l l')->(In x l')->(x=y)\/(In x l).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: or (@eq A x y) (@In A x l) *)
  induction H;simpl in H0.
(* Goal: @Permutation A l (@app A l1 l2) *)
  case H0;intro H1;try (symmetry in H1);tauto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  case H0;simpl;intro;tauto.
Qed.

(** a list is a set iff all the elements are pairwise distinct *)
Inductive is_set (A:Set) : list A->Prop :=
  nil_is_set : (is_set A nil)
|cons_is_set : forall (x:A)(l:list A),(is_set A l)->~(In x l)->(is_set A (x::l)).

(** if (insertion x l l') and l' is a set then l is a set *)
Lemma is_set_insertion : forall (A:Set)(l l':list A)(x:A),(insertion A x l l')->(is_set A l')->(is_set A l).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction 1;intros.
(* Goal: is_set A l *)
(* Goal: is_set A (@cons A y l) *)
  inversion H;trivial.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
(* Goal: is_set A (@cons A y l) *)
  apply cons_is_set.
(* Goal: is_set A l *)
(* Goal: not (@In A y l) *)
  apply IHinsertion;trivial.
(* Goal: not (@In A y l) *)
  intro;apply H4;apply (insertion_inclusion A x l l');trivial.
Qed.

(** if (insertion x l l') and l' is a set then x is not in l *)
Lemma is_set_insertion_in : forall (A:Set)(l l':list A)(x:A),(insertion A x l l')->(is_set A l')->~(In x l).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction l;simpl;try tauto;intros.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H;rewrite <- H3 in H0;inversion H0.
(* Goal: not (or (@eq A a x) (@In A x l)) *)
(* Goal: not (or (@eq A a x) (@In A x l)) *)
  simpl in H7;trivial.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  intro.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  case H10;intro.
(* Goal: False *)
(* Goal: False *)
  apply H9;rewrite H11;eapply insertion_in;apply H5.
(* Goal: False *)
  elim (IHl l'0 x H5 H8 H11).
Qed.

(** if l is a set, x not in l and (insertion x l l') then l' is a set *)
Lemma insertion_is_set : forall (A:Set)(l:list A),(is_set _ l)->forall (x:A),~(In x l)->forall (l':list A),(insertion _ x l l')->(is_set _ l').
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
(* Goal: is_set A (@cons A y l) *)
  apply cons_is_set.
  apply nil_is_set.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
  inversion H2.
  subst x1.
  subst l0.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  subst l'.
(* Goal: is_set A (@cons A y l) *)
  apply cons_is_set.
  eapply IHis_set.
  apply H0.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  apply head_insertion.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
  subst x1;subst y;subst l0.
(* Goal: is_set A (@cons A y l) *)
  apply cons_is_set.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply IHis_set with x0;auto.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  red;intro.
  apply H1.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: @Permutation A l (@app A l1 l2) *)
  right;auto.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  red;intro.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  case (in_insertion_inv _ _ _ _ _ H7 H3);intro.
  apply H1.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: @Permutation A l (@app A l1 l2) *)
  left;auto.
  apply H0.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
Qed.

(** l' is a permutation of l *)
Inductive is_permutation (A:Set) : list A->list A->Prop :=
  nil_is_permutation : (is_permutation A nil nil)
|cons_is_permutation : forall (l l':list A),(is_permutation A l l')->forall (x:A)(l'':(list A)),(insertion A x l' l'')->(is_permutation A (x::l) l'').

(** if l and l' have the same content and are pairwise distinct then l' is a permutation of l *)
Lemma is_set_eq_impl_permutation : forall (A:Set)(l l':list A),(forall (x:A),(In x l)<->(In x l'))->(is_set A l)->(is_set A l')->(is_permutation A l l').
(* Goal: forall (A : Set) (l l' : list A) (_ : forall x : A, iff (@In A x l) (@In A x l')) (_ : is_set A l) (_ : is_set A l'), is_permutation A l l' *)
  induction l;intros;simpl in H.
(* Goal: is_permutation A (@nil A) l' *)
(* Goal: is_permutation A (@cons A a l) l' *)
  destruct l'.
(* Goal: is_permutation A (@nil A) (@nil A) *)
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  apply nil_is_permutation.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (H a);intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  elim H3;simpl;tauto.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  symmetry in H2;rewrite H2 in H;elim (H a);intros.
(* Goal: is_permutation A (@cons A a l) l' *)
  rewrite H2 in H6;rewrite H2.
(* Goal: @Permutation A l (@app A l1 l2) *)
  assert (In x l');auto.
(* Goal: is_permutation A (@cons A x l) l' *)
  elim (in_insertion A x l' H8).
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  intro l'';intro.
(* Goal: is_permutation A (@cons A x0 (@cons A x l)) l3 *)
(* Goal: is_permutation A (@cons A x l'0) l3 *)
  apply cons_is_permutation with l'';trivial.
(* Goal: is_permutation A l l'' *)
  apply IHl;trivial.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  split;intro.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (H x0);intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  elim (in_insertion_inv A x0 x l'' l');auto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  intro;rewrite H13 in H10;rewrite H2 in H5;tauto.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (H x0);intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  case H12;try tauto.
(* Goal: @In A x0 l' *)
(* Goal: forall _ : @eq A x x0, @In A x0 l *)
(* Goal: is_set A l'' *)
  apply (insertion_inclusion A x l'' l');trivial.
(* Goal: forall _ : @eq A x x0, @In A x0 l *)
(* Goal: is_set A l'' *)
  intro;rewrite <- H13 in H10.
(* Goal: @In A x0 l *)
(* Goal: is_set A l'' *)
  elim (is_set_insertion_in A l'' l' x);trivial.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply is_set_insertion;eauto.
Qed.

(** is_permutation is reflexive *)
Lemma is_permutation_refl : forall (A:Set)(l:list A),(is_permutation A l l).
(* Goal: forall (A : Set) (l : list A), is_permutation A l l *)
  induction l.
(* Goal: is_permutation A (@nil A) (@nil A) *)
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  apply nil_is_permutation.
(* Goal: is_permutation A (@cons A a l) (@cons A a l) *)
  eapply cons_is_permutation;[apply IHl | apply head_insertion].
Qed.

(** if l' is l where x has been inserted then l' is a permutation of x::l *)
Lemma insertion_is_permutation : forall (A:Set)(l l':list A)(x:A),(insertion A x l l')->(is_permutation A (x::l) l').
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: is_permutation A (@cons A x l) (@cons A x l) *)
(* Goal: is_permutation A (@cons A x (@cons A y l)) (@cons A y l') *)
  apply cons_is_permutation with l;[apply is_permutation_refl | apply head_insertion].
(* Goal: is_permutation A (@cons A x (@cons A y l)) (@cons A y l') *)
  apply cons_is_permutation with (y::l);[apply is_permutation_refl | apply tail_insertion;trivial].
Qed.

(** if l1 is l0 where x has been inserted and l2 is l1 where y has been inserted then there is l3 such that l3 is l0 where y has been inserted and l2 is l3 where x has been inserted *)
Lemma insertion_trans : forall (A:Set)(l0 l1:list A)(x:A),(insertion A x l0 l1)->forall (l2:list A)(y:A),(insertion A y l1 l2)->exists l3:list A,(insertion A y l0 l3)/\(insertion A x l3 l2).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction 1;intros.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  inversion H.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 (@cons A y (@cons A x l)))) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 (@cons A x l'))) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  exists (y::l);split;[apply head_insertion | apply tail_insertion;apply head_insertion].
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 (@cons A x l'))) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  exists l';split;[trivial | apply head_insertion].
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 (@cons A y0 (@cons A y l')))) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 (@cons A y l'0))) *)
  exists (y0::y::l);split;[apply head_insertion | apply tail_insertion;apply tail_insertion;trivial].
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  elim (IHinsertion l'0 y0 H5);intro l3;intro.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H6;intros.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 (@cons A y l'0))) *)
  exists (y::l3);split;[apply tail_insertion | apply tail_insertion];trivial.
Qed.

(** if l1 is a permutation of l0 and then l1 where x has been inserted is a permutation of l0 where x has been inserted *)
Lemma permutation_insertion : forall (A:Set)(l0 l1:list A),(is_permutation A l0 l1)->forall (x:A)(l2 l3:list A),(insertion A x l0 l2)->(insertion A x l1 l3)->(is_permutation A l2 l3).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction 1;intros.
(* Goal: is_permutation A l2 l3 *)
(* Goal: is_permutation A l2 l3 *)
  inversion H;inversion H0;apply is_permutation_refl.
(* Goal: is_permutation A l2 l3 *)
  inversion H1.
(* Goal: is_permutation A (@cons A x0 (@cons A x l)) l3 *)
(* Goal: is_permutation A (@cons A x l'0) l3 *)
  apply cons_is_permutation with l'';trivial.
(* Goal: is_permutation A (@cons A x l) l'' *)
(* Goal: is_permutation A (@cons A x l'0) l3 *)
  apply cons_is_permutation with l';trivial.
(* Goal: is_permutation A (@cons A x l'0) l3 *)
  elim (insertion_trans A l' l'' x H0 l3 x0 H2).
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  intro l4;intro.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H8;intros.
(* Goal: is_permutation A (@cons A x l'0) l3 *)
  apply cons_is_permutation with l4;trivial.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply IHis_permutation;eauto.
Qed.

(** is_permutation is symmetric *)
Lemma is_permutation_sym : forall (A:Set)(l l':list A),(is_permutation A l l')->(is_permutation A l' l).
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), is_permutation A l' l *)
  induction 1;[apply nil_is_permutation | eapply permutation_insertion;eauto;apply head_insertion].
Qed.

Lemma permutation_in : forall (A:Set)(l l':list A),(is_permutation A l l')->forall (x:A),(In x l)<->(In x l').
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction l;simpl;intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  inversion H;simpl;tauto.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  inversion H;simpl.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  split;intro.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  case H5;intro.
(* Goal: @In A x l' *)
(* Goal: @In A x l' *)
(* Goal: or (@eq A a x) (@In A x l) *)
  eapply insertion_in;rewrite H6 in H4;apply H4.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (IHl l'0 H2 x);intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply insertion_inclusion;eauto.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  case (in_insertion_inv A x a l'0 l' H4 H5);intro.
(* Goal: @Permutation A l (@app A l1 l2) *)
  rewrite H6;tauto.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (IHl l'0 H2 x);intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  right;auto.
Qed.

Lemma permutation_insertion_aux : forall (A:Set)(l l' l'':list A)(x:A),(insertion A x l l')->(insertion A x l l'')->(is_permutation A l' l'').
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply permutation_insertion;eauto.
(* Goal: is_permutation A l l *)
(* Goal: is_permutation A l (@cons A a l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  apply is_permutation_refl.
Qed.

Lemma length_recursion : forall (A:Set),forall (P:list A->Prop),(forall (x:list A),(forall (y:list A),(length y)<(length x)->(P y))->(P x))->(forall (a:list A),(P a)).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @Permutation A l (@app A l1 l2) *)
  apply (well_founded_ind (well_founded_ltof (list A) (fun l:list A => length l)));unfold ltof;auto.
Qed.

Lemma insertion_length : forall (A:Set)(l l':list A)(x:A),(insertion A x l l')->(length l')=(S (length l)).
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @eq nat (@length A l) (@length A l') *)
  induction 1;simpl;trivial.
(* Goal: @eq nat (S (@length A l')) (S (S (@length A l))) *)
  rewrite IHinsertion;trivial.
Qed.

Lemma permutation_length : forall (A:Set)(l l':list A),(is_permutation A l l')->(length l)=(length l').
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @eq nat (@length A l) (@length A l') *)
  induction 1;simpl;trivial.
(* Goal: @eq nat (S (@length A l)) (@length A l'') *)
  generalize (insertion_length A l' l'' x H0);intro;congruence.
Qed.

Lemma insertion_permutation_eq : forall (A:Set)(l l':list A)(x:A),(insertion A x l' l)->forall (l'':list A),(insertion A x l'' l)->(is_permutation A l' l'').
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  induction l;intros;inversion H.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
(* Goal: is_permutation A l l *)
(* Goal: is_permutation A l (@cons A a l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  apply is_permutation_refl.
(* Goal: is_permutation A l (@cons A a l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  rewrite <- H4;destruct l.
(* Goal: is_permutation A (@nil A) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H8.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  generalize (head_insertion A a0 l);intro.
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  assert (In x (a0::l)).
(* Goal: @In A x (@cons A a0 l) *)
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  eapply insertion_in;apply H8.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  case (in_insertion_inv A x a0 l (a0::l) H10 H11);intro.
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  rewrite H12;rewrite <- H12 in H10;rewrite <- H12 in H8;rewrite <- H12 in IHl.
(* Goal: is_permutation A (@cons A a0 l) (@cons A a0 l1) *)
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  assert (is_permutation A l l1).
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply IHl;eauto.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  eapply cons_is_permutation;eauto;apply head_insertion.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  elim (in_insertion A x l H12);intro l2;intro.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  generalize (tail_insertion A x a0 l2 l H13);intro.
(* Goal: is_permutation A (@cons A a0 l) (@cons A x l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  assert (is_permutation A (a0::l2) l1).
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply IHl;eauto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  apply is_permutation_sym;auto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply cons_is_permutation;eauto.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  rewrite H1 in H3.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
(* Goal: is_permutation A (@cons A a l0) l *)
(* Goal: is_permutation A (@cons A a l0) (@cons A a l1) *)
  rewrite <- H9;apply insertion_is_permutation;trivial.
(* Goal: is_permutation A (@cons A a l0) (@cons A a l1) *)
  assert (is_permutation A l0 l1).
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply IHl;eauto.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  eapply cons_is_permutation;eauto;apply head_insertion.
Qed.

Lemma permutation_insertion_comm : forall (A:Set)(l1 l2:list A)(x:A),(insertion A x l1 l2)->forall (l4:list A),(is_permutation A l2 l4)->(exists l3:list A,(is_permutation A l1 l3) /\ (insertion A x l3 l4)).
  intros A l1 l2.
  generalize l1;clear l1.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction l2;intros.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  inversion H.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  inversion H.
  subst a.
  subst x0.
  subst l.
  subst l2.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
  subst x0.
  subst l.
  subst l''.
  exists l'.
(* Goal: @Permutation A l (@app A l1 l2) *)
  tauto.
  subst x0.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  subst l'.
  subst a.
  subst l1.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  inversion H0.
  subst x0.
  subst l''.
  subst l0.
  elim (IHl2 l x H4 l' H3).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro l3;intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H1;clear H1;intros.
  elim (insertion_trans A l3 l' x H2 l4 y H6).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro l5;intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H5;clear H5;intros.
  exists l5.
  split;trivial.
  eapply cons_is_permutation.
  apply H1.
(* Goal: is_permutation A l l' *)
  trivial.
Qed.

Lemma permutation_insertion_permutation : forall (A:Set)(l l':list A),(is_permutation A l l')->forall (x:A)(l'':list A),(insertion A x l' l'')->forall (l''':list A),(is_permutation A l'' l''')->(is_permutation A (x::l) l''').
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction 1;intros.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  inversion H.
  rewrite <- H3 in H0.
(* Goal: is_permutation A l l' *)
  trivial.
  elim (permutation_insertion_comm A l'' l''0 x0 H1 l''' H2).
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  intro l1;intro.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H3;clear H3;intros.
  eapply cons_is_permutation.
  eapply IHis_permutation.
  apply H0.
  apply H3.
(* Goal: is_permutation A l l' *)
  trivial.
Qed.

(** is_permutation is transitive *)
Lemma is_permutation_trans : forall (A:Set)(l l':list A),(is_permutation A l l')->forall (l'':list A),(is_permutation A l' l'')->(is_permutation A l l'').
(* Goal: forall (A : Set) (l : list A), is_permutation A l l *)
  induction l.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  inversion H.
(* Goal: is_permutation A l l' *)
  rewrite <- H2 in H0;trivial.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y l l3) (insertion A x l3 l2)) *)
(* Goal: @ex (list A) (fun l3 : list A => and (insertion A y0 (@cons A y l) l3) (insertion A x l3 l2)) *)
  inversion H.
(* Goal: is_permutation A (@cons A a l0) l'' *)
  induction H5;inversion H0.
(* Goal: is_permutation A l l' *)
  eapply cons_is_permutation;try (apply IHl with l1;eauto);trivial.
  eapply permutation_insertion_permutation.
  apply H3.
(* Goal: insertion A x0 (@cons A a xs) (@cons A a xss) *)
  apply tail_insertion.
  apply H5.
  eapply cons_is_permutation.
  apply H8.
  apply H10.
Qed.

Lemma is_permutation_reverse : forall (A:Set)(l:list A),(is_permutation A l (rev l)).
(* Goal: forall (A : Set) (l : list A), is_permutation A l l *)
  induction l.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: is_permutation A (@nil A) (@nil A) *)
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  apply nil_is_permutation.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
  eapply cons_is_permutation.
  apply IHl.
  apply insertion_snoc.
Qed.

Lemma is_permutation_reverse_impl_is_permutation : forall (A:Set)(l l':list A),(is_permutation A (rev l) (rev l'))->(is_permutation A l l').
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
  eapply is_permutation_trans.
  apply is_permutation_reverse.
  apply is_permutation_sym.
  eapply is_permutation_trans.
  apply is_permutation_reverse.
  apply is_permutation_sym.
(* Goal: is_permutation A l l' *)
  trivial.
Qed.

Lemma is_permutation_impl_is_permutation_reverse : forall (A:Set)(l l':list A),(is_permutation A l l')->(is_permutation A (rev l) (rev l')).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: is_permutation A (@rev A l) (@rev A l') *)
  apply is_permutation_reverse_impl_is_permutation.
(* Goal: is_permutation A l (@rev A (@rev A l')) *)
  rewrite rev_involutive.
(* Goal: is_permutation A l (@rev A (@rev A l')) *)
  rewrite rev_involutive.
(* Goal: is_permutation A l l' *)
  trivial.
Qed.

Lemma is_permutation_cons_snoc : forall (A:Set)(x:A)(xs:list A),(is_permutation A (cons x xs) (app xs (cons x nil))).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
  eapply cons_is_permutation.
(* Goal: is_permutation A l l *)
(* Goal: is_permutation A l (@cons A a l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  apply is_permutation_refl.
  apply insertion_snoc.
Qed.

Lemma insertion_append : forall (A:Set)(x:A)(xs xss:list A),(insertion A x xs xss)->forall (yss:list A),(insertion A x (app xs yss) (app xss yss)).
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  apply head_insertion.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: insertion A x0 (@cons A a xs) (@cons A a xss) *)
  apply tail_insertion.
(* Goal: insertion A x (@app A l yss) (@app A l' yss) *)
  apply IHinsertion.
Qed.

Lemma is_permutation_append : forall (A:Set)(xs ys:list A),(is_permutation A xs ys)->forall (xs' ys':list A),(is_permutation A xs' ys')->(is_permutation A (app xs xs') (app ys ys')).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction 1;intros.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
  eapply cons_is_permutation.
  apply IHis_permutation.
  apply H1.
  apply insertion_append.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
Qed.

Lemma insertion_map : forall (B:Set)(y:B)(ys yss:list B),(insertion _ y ys yss)->forall (A:Set)(f:A->B)(x:A),y=f x->forall (xs:list A),ys = map f xs->exists xss:list A,yss = map f xss /\ insertion _ x xs xss.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  induction 1;intros.
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B x l) (@map A B f xss)) (insertion A x0 xs xss)) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  exists (cons x0 xs).
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: and (is_permutation A (@nil A) (@nil A)) (@eq (list B) (@nil B) (@map A B f (@nil A))) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  split.
(* Goal: @Permutation A l (@app A l1 l2) *)
  subst x;subst l;auto.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  apply head_insertion.
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  destruct xs.
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 (@nil A) xss)) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 (@cons A a xs) xss)) *)
  discriminate H1.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  simpl in H1.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  injection H1;clear H1;intros.
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 (@cons A a xs) xss)) *)
  elim (IHinsertion _ _ _ H0 _ H1).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro xss;intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H3;clear H3;intros.
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 (@cons A a xs) xss)) *)
  exists (cons a xss).
(* Goal: and (@eq (list B) (@cons B y l') (@map A B f (@cons A a xss))) (insertion A x0 (@cons A a xs) (@cons A a xss)) *)
  simpl.
(* Goal: and (is_permutation A (@nil A) (@nil A)) (@eq (list B) (@nil B) (@map A B f (@nil A))) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  split.
(* Goal: @Permutation A l (@app A l1 l2) *)
  subst y;subst l';auto.
(* Goal: insertion A x0 (@cons A a xs) (@cons A a xss) *)
  apply tail_insertion.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
Qed.

Lemma is_permutation_map : forall (B:Set)(ys1 ys2:list B),(is_permutation B ys1 ys2)->forall (A:Set)(f:A->B)(xs1:list A),(ys1 = map f xs1)->exists xs2:list A,(is_permutation A xs1 xs2)/\ys2 = map f xs2.
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) (@nil B) (@map A B f xs2))) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  destruct xs1;try (discriminate H).
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) (@cons A x l) (@app A l1 (@cons A x l2))))) *)
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  exists (nil (A:=A)).
(* Goal: and (is_permutation A (@nil A) (@nil A)) (@eq (list B) (@nil B) (@map A B f (@nil A))) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  split.
(* Goal: is_permutation A (@nil A) (@nil A) *)
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  apply nil_is_permutation.
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  reflexivity.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  destruct xs1;try (discriminate H1).
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  simpl in H1.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  injection H1;clear H1;intros.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  subst x.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (IHis_permutation _ _ _ H1).
(* Goal: forall (x : list A) (_ : and (is_permutation A xs1 x) (@eq (list B) l' (@map A B f x))), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro xs2.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H2;clear H2;intros.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  subst l'.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim (insertion_map _ _ _ _ H0 _ f a (refl_equal (f a)) xs2 (refl_equal (map f xs2))).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H3;clear H3;intros.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  exists x.
(* Goal: @Permutation A l (@app A l1 l2) *)
  split;auto.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply cons_is_permutation;eauto.
Qed.

(** if l' is a permutation of l and the elements of l are pairwise distinct, then so are those of l' *)
Lemma is_permutation_set : forall (A:Set)(l l':list A),(is_permutation _ l l')->(is_set _ l)->(is_set _ l').
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: is_permutation A l2 l3 *)
  inversion H1.
  subst x0;subst l0.
  eapply insertion_is_set.
  apply IHis_permutation.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
  elim (permutation_in _ _ _ H x).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intros.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  red;intro.
  apply H5.
  apply H3.
  apply H6.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
Qed.

Lemma Permutation_impl_permutation : forall (A:Set)(l l':list A),(Permutation l l')->(is_permutation _ l l').
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: is_permutation A (@nil A) (@nil A) *)
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  apply nil_is_permutation.
  eapply cons_is_permutation.
  apply IHPermutation.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  apply head_insertion.
  eapply cons_is_permutation.
(* Goal: is_permutation A l l *)
(* Goal: is_permutation A l (@cons A a l1) *)
(* Goal: is_permutation A (@cons A a l0) l'' *)
  apply is_permutation_refl.
(* Goal: insertion A x0 (@cons A a xs) (@cons A a xss) *)
  apply tail_insertion.
(* Goal: insertion A x0 xs (@cons A x0 xs) *)
(* Goal: @ex (list A) (fun xss : list A => and (@eq (list B) (@cons B y l') (@map A B f xss)) (insertion A x0 xs xss)) *)
  apply head_insertion.
(* Goal: @Permutation A l (@app A l1 l2) *)
  eapply is_permutation_trans;eauto.
Qed.

Lemma insertion_append_decompose : forall (A:Set)(x:A)(l l':list A),(insertion _ x l l')->exists l1:list A,exists l2:list A,l=(app l1 l2)/\l'=(app l1 (cons x l2)).
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) (@cons A x l) (@app A l1 (@cons A x l2))))) *)
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  exists (nil (A:=A)).
(* Goal: @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A (@nil A) l2)) (@eq (list A) (@cons A x l) (@app A (@nil A) (@cons A x l2)))) *)
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  exists l.
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  split;try reflexivity.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  elim IHinsertion.
(* Goal: forall (x0 : list A) (_ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A x0 l2)) (@eq (list A) l' (@app A x0 (@cons A x l2))))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  intro l1.
(* Goal: forall _ : @ex (list A) (fun l2 : list A => and (@eq (list A) l (@app A l1 l2)) (@eq (list A) l' (@app A l1 (@cons A x l2)))), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  intro.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  elim H0.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro l2;intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H1;clear H1;intros.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A l1 l2)) (@eq (list A) (@cons A y l') (@app A l1 (@cons A x l2))))) *)
  exists (cons y l1).
(* Goal: @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A y l) (@app A (@cons A y l1) l2)) (@eq (list A) (@cons A y l') (@app A (@cons A y l1) (@cons A x l2)))) *)
  exists l2.
(* Goal: @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  subst l;subst l'.
(* Goal: @eq (list B) (@nil B) (@map A B f (@nil A)) *)
(* Goal: forall (A : Set) (f : forall _ : A, B) (xs1 : list A) (_ : @eq (list B) (@cons B x l) (@map A B f xs1)), @ex (list A) (fun xs2 : list A => and (is_permutation A xs1 xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  split;try reflexivity.
Qed.

Lemma permutation_impl_Permutation : forall (A:Set)(l l':list A),(is_permutation _ l l')->(Permutation l l').
(* Goal: forall (A : Set) (l l' : list A) (_ : is_permutation A l l'), @Permutation A l l' *)
  induction 1.
(* Goal: @Permutation A (@nil A) (@nil A) *)
(* Goal: @Permutation A (@cons A x l) l'' *)
  apply perm_nil.
(* Goal: @Permutation A (@cons A x l) l'' *)
  elim (insertion_append_decompose _ _ _ _ H0).
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro l1;intros.
(* Goal: @Permutation A (@cons A x l) l'' *)
  elim H1.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  intro l2;intros.
(* Goal: forall (x : list A) (_ : and (@eq (list B) l'' (@map A B f x)) (insertion A a xs2 x)), @ex (list A) (fun xs2 : list A => and (is_permutation A (@cons A a xs1) xs2) (@eq (list B) l'' (@map A B f xs2))) *)
  elim H2;clear H2;intros.
  subst l';subst l''.
(* Goal: @Permutation A (@cons A x l) (@app A l1 (@cons A x l2)) *)
  apply Permutation_cons_app.
(* Goal: @Permutation A l (@app A l1 l2) *)
  auto.
Qed.

