(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Permutation SetoidList.
(* Set Universe Polymorphism. *)

Set Implicit Arguments.
Unset Strict Implicit.

Section Permutation.
Context {A : Type} (eqA : relation A) (e : Equivalence eqA).

Inductive PermutationA : list A -> list A -> Prop :=
  | permA_nil: PermutationA nil nil
  | permA_skip x₁ x₂ l₁ l₂ :
     eqA x₁ x₂ -> PermutationA l₁ l₂ -> PermutationA (x₁ :: l₁) (x₂ :: l₂)
  | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l)
  | permA_trans l₁ l₂ l₃ :
     PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃.
Local Hint Constructors PermutationA : core.

Global Instance: Equivalence PermutationA.
A:Type
eqA:relation A
e:Equivalence eqA
Equivalence PermutationA
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
Equivalence PermutationA
 constructor.
A:Type
eqA:relation A
e:Equivalence eqA
Reflexive PermutationA
A:Type
eqA:relation A
e:Equivalence eqA
Symmetric PermutationA
A:Type
eqA:relation A
e:Equivalence eqA
Transitive PermutationA
 -
A:Type
eqA:relation A
e:Equivalence eqA
Reflexive PermutationA intro l.
A:Type
eqA:relation A
e:Equivalence eqA
l:list A
PermutationA l l induction l; intuition.
 -
A:Type
eqA:relation A
e:Equivalence eqA
Symmetric PermutationA intros l₁ l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ -> PermutationA l₂ l₁ induction 1; eauto.
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:PermutationA l₂ l₁
PermutationA (x₂ :: l₂) (x₁ :: l₁) apply permA_skip; intuition.
 -
A:Type
eqA:relation A
e:Equivalence eqA
Transitive PermutationA exact permA_trans.
Qed.

Instance PermutationA_cons :
  Proper (eqA ==> PermutationA ==> PermutationA) (@cons A).
A:Type
eqA:relation A
e:Equivalence eqA
Proper (eqA ==> PermutationA ==> PermutationA) cons
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
Proper (eqA ==> PermutationA ==> PermutationA) cons
 repeat intro.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
H:eqA x y
x0, y0:list A
H0:PermutationA x0 y0
PermutationA (x :: x0) (y :: y0) now apply permA_skip.
Qed.

Lemma PermutationA_app_head l₁ l₂ l :
  PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l:list A
PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂)
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l:list A
PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂)
 induction l; trivial; intros.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
a:A
l:list A
IHl:PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂)
H:PermutationA l₁ l₂
PermutationA ((a :: l) ++ l₁) ((a :: l) ++ l₂) apply permA_skip; intuition.
Qed.

Instance PermutationA_app :
  Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
A:Type
eqA:relation A
e:Equivalence eqA
Proper
  (PermutationA ==> PermutationA ==> PermutationA)
  (app (A:=A))
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
Proper
  (PermutationA ==> PermutationA ==> PermutationA)
  (app (A:=A))
 intros l₁ l₂ Pl k₁ k₂ Pk.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
Pl:PermutationA l₁ l₂
k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
 induction Pl.
A:Type
eqA:relation A
e:Equivalence eqA
k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA (nil ++ k₁) (nil ++ k₂)
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
Pl:PermutationA l₁ l₂
k₁, k₂:list A
Pk:PermutationA k₁ k₂
IHPl:PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
PermutationA ((x₁ :: l₁) ++ k₁) ((x₂ :: l₂) ++ k₂)
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA ((y :: x :: l) ++ k₁)
  ((x :: y :: l) ++ k₂)
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
Pl1:PermutationA l₁ l₂
Pl2:PermutationA l₂ l₃
k₁, k₂:list A
Pk:PermutationA k₁ k₂
IHPl1:PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
IHPl2:PermutationA (l₂ ++ k₁) (l₃ ++ k₂)
PermutationA (l₁ ++ k₁) (l₃ ++ k₂)
 -
A:Type
eqA:relation A
e:Equivalence eqA
k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA (nil ++ k₁) (nil ++ k₂) easy.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
Pl:PermutationA l₁ l₂
k₁, k₂:list A
Pk:PermutationA k₁ k₂
IHPl:PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
PermutationA ((x₁ :: l₁) ++ k₁) ((x₂ :: l₂) ++ k₂) now apply permA_skip.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA ((y :: x :: l) ++ k₁)
  ((x :: y :: l) ++ k₂) etransitivity.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA ((y :: x :: l) ++ k₁) ?y
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA ?y ((x :: y :: l) ++ k₂)
   *
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA ((y :: x :: l) ++ k₁) ?y rewrite <-!app_comm_cons.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA (y :: x :: l ++ k₁) ?y now apply permA_swap.
   *
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA (x :: y :: l ++ k₁) ((x :: y :: l) ++ k₂) rewrite !app_comm_cons.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, k₁, k₂:list A
Pk:PermutationA k₁ k₂
PermutationA ((x :: y :: l) ++ k₁)
  ((x :: y :: l) ++ k₂) now apply PermutationA_app_head.
 -
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
Pl1:PermutationA l₁ l₂
Pl2:PermutationA l₂ l₃
k₁, k₂:list A
Pk:PermutationA k₁ k₂
IHPl1:PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
IHPl2:PermutationA (l₂ ++ k₁) (l₃ ++ k₂)
PermutationA (l₁ ++ k₁) (l₃ ++ k₂) do 2 (etransitivity; try eassumption).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
Pl1:PermutationA l₁ l₂
Pl2:PermutationA l₂ l₃
k₁, k₂:list A
Pk:PermutationA k₁ k₂
IHPl1:PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
IHPl2:PermutationA (l₂ ++ k₁) (l₃ ++ k₂)
PermutationA (l₂ ++ k₂) (l₂ ++ k₁)
   apply PermutationA_app_head.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
Pl1:PermutationA l₁ l₂
Pl2:PermutationA l₂ l₃
k₁, k₂:list A
Pk:PermutationA k₁ k₂
IHPl1:PermutationA (l₁ ++ k₁) (l₂ ++ k₂)
IHPl2:PermutationA (l₂ ++ k₁) (l₃ ++ k₂)
PermutationA k₂ k₁ now symmetry.
Qed.

Lemma PermutationA_app_tail l₁ l₂ l :
  PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l:list A
PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l)
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l:list A
PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l)
 intros E.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l:list A
E:PermutationA l₁ l₂
PermutationA (l₁ ++ l) (l₂ ++ l) now rewrite E.
Qed.

Lemma PermutationA_cons_append l x :
  PermutationA (x :: l) (l ++ x :: nil).
A:Type
eqA:relation A
e:Equivalence eqA
l:list A
x:A
PermutationA (x :: l) (l ++ x :: nil)
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l:list A
x:A
PermutationA (x :: l) (l ++ x :: nil)
 induction l.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
PermutationA (x :: nil) (nil ++ x :: nil)
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l:list A
x:A
IHl:PermutationA (x :: l) (l ++ x :: nil)
PermutationA (x :: a :: l) ((a :: l) ++ x :: nil)
 -
A:Type
eqA:relation A
e:Equivalence eqA
x:A
PermutationA (x :: nil) (nil ++ x :: nil) easy.
 -
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l:list A
x:A
IHl:PermutationA (x :: l) (l ++ x :: nil)
PermutationA (x :: a :: l) ((a :: l) ++ x :: nil) simpl.
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l:list A
x:A
IHl:PermutationA (x :: l) (l ++ x :: nil)
PermutationA (x :: a :: l) (a :: l ++ x :: nil) rewrite <-IHl.
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l:list A
x:A
IHl:PermutationA (x :: l) (l ++ x :: nil)
PermutationA (x :: a :: l) (a :: x :: l) intuition.
Qed.

Lemma PermutationA_app_comm l₁ l₂ :
  PermutationA (l₁ ++ l₂) (l₂ ++ l₁).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA (l₁ ++ l₂) (l₂ ++ l₁)
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA (l₁ ++ l₂) (l₂ ++ l₁)
 induction l₁.
A:Type
eqA:relation A
e:Equivalence eqA
l₂:list A
PermutationA (nil ++ l₂) (l₂ ++ nil)
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l₁, l₂:list A
IHl₁:PermutationA (l₁ ++ l₂) (l₂ ++ l₁)
PermutationA ((a :: l₁) ++ l₂) (l₂ ++ a :: l₁)
 -
A:Type
eqA:relation A
e:Equivalence eqA
l₂:list A
PermutationA (nil ++ l₂) (l₂ ++ nil) now rewrite app_nil_r.
 -
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l₁, l₂:list A
IHl₁:PermutationA (l₁ ++ l₂) (l₂ ++ l₁)
PermutationA ((a :: l₁) ++ l₂) (l₂ ++ a :: l₁) rewrite <-app_comm_cons, IHl₁, app_comm_cons.
A:Type
eqA:relation A
e:Equivalence eqA
a:A
l₁, l₂:list A
IHl₁:PermutationA (l₁ ++ l₂) (l₂ ++ l₁)
PermutationA ((a :: l₂) ++ l₁) (l₂ ++ a :: l₁)
   now rewrite PermutationA_cons_append, <-app_assoc.
Qed.

Lemma PermutationA_cons_app l l₁ l₂ x :
  PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂).
A:Type
eqA:relation A
e:Equivalence eqA
l, l₁, l₂:list A
x:A
PermutationA l (l₁ ++ l₂) ->
PermutationA (x :: l) (l₁ ++ x :: l₂)
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l, l₁, l₂:list A
x:A
PermutationA l (l₁ ++ l₂) ->
PermutationA (x :: l) (l₁ ++ x :: l₂)
 intros E.
A:Type
eqA:relation A
e:Equivalence eqA
l, l₁, l₂:list A
x:A
E:PermutationA l (l₁ ++ l₂)
PermutationA (x :: l) (l₁ ++ x :: l₂) rewrite E.
A:Type
eqA:relation A
e:Equivalence eqA
l, l₁, l₂:list A
x:A
E:PermutationA l (l₁ ++ l₂)
PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂)
 now rewrite app_comm_cons, (PermutationA_cons_append l₁ x), <- app_assoc.
Qed.

Lemma PermutationA_middle l₁ l₂ x :
  PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
x:A
PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂)
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
x:A
PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂)
 now apply PermutationA_cons_app.
Qed.

Lemma PermutationA_equivlistA l₁ l₂ :
  PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂
 induction 1.
A:Type
eqA:relation A
e:Equivalence eqA
equivlistA eqA nil nil
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:equivlistA eqA l₁ l₂
equivlistA eqA (x₁ :: l₁) (x₂ :: l₂)
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
equivlistA eqA (y :: x :: l) (x :: y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
IHPermutationA1:equivlistA eqA l₁ l₂
IHPermutationA2:equivlistA eqA l₂ l₃
equivlistA eqA l₁ l₃
 -
A:Type
eqA:relation A
e:Equivalence eqA
equivlistA eqA nil nil reflexivity.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:equivlistA eqA l₁ l₂
equivlistA eqA (x₁ :: l₁) (x₂ :: l₂) now apply equivlistA_cons_proper.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
equivlistA eqA (y :: x :: l) (x :: y :: l) now apply equivlistA_permute_heads.
 -
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
IHPermutationA1:equivlistA eqA l₁ l₂
IHPermutationA2:equivlistA eqA l₂ l₃
equivlistA eqA l₁ l₃ etransitivity; eassumption.
Qed.

Lemma NoDupA_equivlistA_PermutationA l₁ l₂ :
  NoDupA eqA l₁ -> NoDupA eqA l₂ ->
   equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
NoDupA eqA l₁ ->
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
NoDupA eqA l₁ ->
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
  intros Pl₁.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
Pl₁:NoDupA eqA l₁
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂ revert l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁:list A
Pl₁:NoDupA eqA l₁
forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂ induction Pl₁ as [|x l₁ E1].
A:Type
eqA:relation A
e:Equivalence eqA
forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA nil l₂ -> PermutationA nil l₂
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA (x :: l₁) l₂ ->
PermutationA (x :: l₁) l₂
  -
A:Type
eqA:relation A
e:Equivalence eqA
forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA nil l₂ -> PermutationA nil l₂ intros l₂ _ H₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₂:list A
H₂:equivlistA eqA nil l₂
PermutationA nil l₂ symmetry in H₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₂:list A
H₂:equivlistA eqA l₂ nil
PermutationA nil l₂ now rewrite (equivlistA_nil_eq eqA).
  -
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA (x :: l₁) l₂ ->
PermutationA (x :: l₁) l₂ intros l₂ Pl₂ E2.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂0 : list A,
NoDupA eqA l₂0 ->
equivlistA eqA l₁ l₂0 -> PermutationA l₁ l₂0
l₂:list A
Pl₂:NoDupA eqA l₂
E2:equivlistA eqA (x :: l₁) l₂
PermutationA (x :: l₁) l₂
    destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]].
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂0 : list A,
NoDupA eqA l₂0 ->
equivlistA eqA l₁ l₂0 -> PermutationA l₁ l₂0
l₂:list A
Pl₂:NoDupA eqA l₂
E2:equivlistA eqA (x :: l₁) l₂
InA eqA x l₂
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂0 : list A,
NoDupA eqA l₂0 ->
equivlistA eqA l₁ l₂0 -> PermutationA l₁ l₂0
l₂:list A
Pl₂:NoDupA eqA l₂
E2:equivlistA eqA (x :: l₁) l₂
l₂h:list A
y:A
l₂t:list A
E3:eqA x y
H:l₂ = l₂h ++ y :: l₂t
PermutationA (x :: l₁) l₂
    {
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂0 : list A,
NoDupA eqA l₂0 ->
equivlistA eqA l₁ l₂0 -> PermutationA l₁ l₂0
l₂:list A
Pl₂:NoDupA eqA l₂
E2:equivlistA eqA (x :: l₁) l₂
InA eqA x l₂ rewrite <-E2.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂0 : list A,
NoDupA eqA l₂0 ->
equivlistA eqA l₁ l₂0 -> PermutationA l₁ l₂0
l₂:list A
Pl₂:NoDupA eqA l₂
E2:equivlistA eqA (x :: l₁) l₂
InA eqA x (x :: l₁) intuition. }
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂0 : list A,
NoDupA eqA l₂0 ->
equivlistA eqA l₁ l₂0 -> PermutationA l₁ l₂0
l₂:list A
Pl₂:NoDupA eqA l₂
E2:equivlistA eqA (x :: l₁) l₂
l₂h:list A
y:A
l₂t:list A
E3:eqA x y
H:l₂ = l₂h ++ y :: l₂t
PermutationA (x :: l₁) l₂
    subst.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
l₂h:list A
y:A
l₂t:list A
E2:equivlistA eqA (x :: l₁) (l₂h ++ y :: l₂t)
Pl₂:NoDupA eqA (l₂h ++ y :: l₂t)
E3:eqA x y
PermutationA (x :: l₁) (l₂h ++ y :: l₂t) transitivity (y :: l₁); [intuition |].
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
l₂h:list A
y:A
l₂t:list A
E2:equivlistA eqA (x :: l₁) (l₂h ++ y :: l₂t)
Pl₂:NoDupA eqA (l₂h ++ y :: l₂t)
E3:eqA x y
PermutationA (y :: l₁) (l₂h ++ y :: l₂t)
    apply PermutationA_cons_app, IHPl₁.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
l₂h:list A
y:A
l₂t:list A
E2:equivlistA eqA (x :: l₁) (l₂h ++ y :: l₂t)
Pl₂:NoDupA eqA (l₂h ++ y :: l₂t)
E3:eqA x y
NoDupA eqA (l₂h ++ l₂t)
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
l₂h:list A
y:A
l₂t:list A
E2:equivlistA eqA (x :: l₁) (l₂h ++ y :: l₂t)
Pl₂:NoDupA eqA (l₂h ++ y :: l₂t)
E3:eqA x y
equivlistA eqA l₁ (l₂h ++ l₂t)
    now apply NoDupA_split with y.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l₁:list A
E1:~ InA eqA x l₁
Pl₁:NoDupA eqA l₁
IHPl₁:forall l₂ : list A,
NoDupA eqA l₂ ->
equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂
l₂h:list A
y:A
l₂t:list A
E2:equivlistA eqA (x :: l₁) (l₂h ++ y :: l₂t)
Pl₂:NoDupA eqA (l₂h ++ y :: l₂t)
E3:eqA x y
equivlistA eqA l₁ (l₂h ++ l₂t)
    apply equivlistA_NoDupA_split with x y; intuition.
Qed.

Lemma Permutation_eqlistA_commute l₁ l₂ l₃ :
 eqlistA eqA l₁ l₂ -> Permutation l₂ l₃ ->
 exists l₂', Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
eqlistA eqA l₁ l₂ ->
Permutation l₂ l₃ ->
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
eqlistA eqA l₁ l₂ ->
Permutation l₂ l₃ ->
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃
 intros E P.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
E:eqlistA eqA l₁ l₂
P:Permutation l₂ l₃
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃ revert l₁ E.
A:Type
eqA:relation A
e:Equivalence eqA
l₂, l₃:list A
P:Permutation l₂ l₃
forall l₁ : list A,
eqlistA eqA l₁ l₂ ->
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃
 induction P; intros.
A:Type
eqA:relation A
e:Equivalence eqA
l₁:list A
E:eqlistA eqA l₁ nil
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' nil
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
P:Permutation l l'
IHP:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A, Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
l₁:list A
E:eqlistA eqA l₁ (x :: l)
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' (x :: l')
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, l₁:list A
E:eqlistA eqA l₁ (y :: x :: l)
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' (x :: y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l''
l₁:list A
E:eqlistA eqA l₁ l
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l''
 -
A:Type
eqA:relation A
e:Equivalence eqA
l₁:list A
E:eqlistA eqA l₁ nil
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' nil inversion_clear E.
A:Type
eqA:relation A
e:Equivalence eqA
l₁:list A
exists l₂' : list A,
  Permutation nil l₂' /\ eqlistA eqA l₂' nil now exists nil.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
P:Permutation l l'
IHP:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A, Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
l₁:list A
E:eqlistA eqA l₁ (x :: l)
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' (x :: l') inversion_clear E.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
P:Permutation l l'
IHP:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A, Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
l₁:list A
x0:A
l0:list A
H:eqA x0 x
H0:eqlistA eqA l0 l
exists l₂' : list A,
  Permutation (x0 :: l0) l₂' /\
  eqlistA eqA l₂' (x :: l')
   destruct (IHP l0) as (l0',(P',E')); trivial.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
P:Permutation l l'
IHP:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A, Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
l₁:list A
x0:A
l0:list A
H:eqA x0 x
H0:eqlistA eqA l0 l
l0':list A
P':Permutation l0 l0'
E':eqlistA eqA l0' l'
exists l₂' : list A,
  Permutation (x0 :: l0) l₂' /\
  eqlistA eqA l₂' (x :: l') clear IHP.
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
P:Permutation l l'
l₁:list A
x0:A
l0:list A
H:eqA x0 x
H0:eqlistA eqA l0 l
l0':list A
P':Permutation l0 l0'
E':eqlistA eqA l0' l'
exists l₂' : list A,
  Permutation (x0 :: l0) l₂' /\
  eqlistA eqA l₂' (x :: l')
   exists (x0::l0').
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
P:Permutation l l'
l₁:list A
x0:A
l0:list A
H:eqA x0 x
H0:eqlistA eqA l0 l
l0':list A
P':Permutation l0 l0'
E':eqlistA eqA l0' l'
Permutation (x0 :: l0) (x0 :: l0') /\
eqlistA eqA (x0 :: l0') (x :: l') split; auto.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, l₁:list A
E:eqlistA eqA l₁ (y :: x :: l)
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' (x :: y :: l) inversion_clear E.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, l₁:list A
x0:A
l0:list A
H:eqA x0 y
H0:eqlistA eqA l0 (x :: l)
exists l₂' : list A,
  Permutation (x0 :: l0) l₂' /\
  eqlistA eqA l₂' (x :: y :: l) inversion_clear H0.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, l₁:list A
x0:A
l0:list A
H:eqA x0 y
x1:A
l1:list A
H1:eqA x1 x
H2:eqlistA eqA l1 l
exists l₂' : list A,
  Permutation (x0 :: x1 :: l1) l₂' /\
  eqlistA eqA l₂' (x :: y :: l)
   exists (x1::x0::l1).
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l, l₁:list A
x0:A
l0:list A
H:eqA x0 y
x1:A
l1:list A
H1:eqA x1 x
H2:eqlistA eqA l1 l
Permutation (x0 :: x1 :: l1) (x1 :: x0 :: l1) /\
eqlistA eqA (x1 :: x0 :: l1) (x :: y :: l) now repeat constructor.
 -
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
P1:Permutation l l'
P2:Permutation l' l''
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l''
l₁:list A
E:eqlistA eqA l₁ l
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l'' clear P1 P2.
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l''
l₁:list A
E:eqlistA eqA l₁ l
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l''
   destruct (IHP1 _ E) as (l₁',(P₁,E₁)).
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂' : list A,
  Permutation l₁0 l₂' /\ eqlistA eqA l₂' l''
l₁:list A
E:eqlistA eqA l₁ l
l₁':list A
P₁:Permutation l₁ l₁'
E₁:eqlistA eqA l₁' l'
exists l₂' : list A,
  Permutation l₁ l₂' /\ eqlistA eqA l₂' l''
   destruct (IHP2 _ E₁) as (l₂',(P₂,E₂)).
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂'0 : list A,
  Permutation l₁0 l₂'0 /\ eqlistA eqA l₂'0 l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂'0 : list A,
  Permutation l₁0 l₂'0 /\ eqlistA eqA l₂'0 l''
l₁:list A
E:eqlistA eqA l₁ l
l₁':list A
P₁:Permutation l₁ l₁'
E₁:eqlistA eqA l₁' l'
l₂':list A
P₂:Permutation l₁' l₂'
E₂:eqlistA eqA l₂' l''
exists l₂'0 : list A,
  Permutation l₁ l₂'0 /\ eqlistA eqA l₂'0 l''
   exists l₂'.
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂'0 : list A,
  Permutation l₁0 l₂'0 /\ eqlistA eqA l₂'0 l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂'0 : list A,
  Permutation l₁0 l₂'0 /\ eqlistA eqA l₂'0 l''
l₁:list A
E:eqlistA eqA l₁ l
l₁':list A
P₁:Permutation l₁ l₁'
E₁:eqlistA eqA l₁' l'
l₂':list A
P₂:Permutation l₁' l₂'
E₂:eqlistA eqA l₂' l''
Permutation l₁ l₂' /\ eqlistA eqA l₂' l'' split; trivial.
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
IHP1:forall l₁0 : list A,
eqlistA eqA l₁0 l ->
exists l₂'0 : list A,
  Permutation l₁0 l₂'0 /\ eqlistA eqA l₂'0 l'
IHP2:forall l₁0 : list A,
eqlistA eqA l₁0 l' ->
exists l₂'0 : list A,
  Permutation l₁0 l₂'0 /\ eqlistA eqA l₂'0 l''
l₁:list A
E:eqlistA eqA l₁ l
l₁':list A
P₁:Permutation l₁ l₁'
E₁:eqlistA eqA l₁' l'
l₂':list A
P₂:Permutation l₁' l₂'
E₂:eqlistA eqA l₂' l''
Permutation l₁ l₂' econstructor; eauto.
Qed.

Lemma PermutationA_decompose l₁ l₂ :
 PermutationA l₁ l₂ ->
 exists l, Permutation l₁ l /\ eqlistA eqA l l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ ->
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₂
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ ->
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₂
 induction 1.
A:Type
eqA:relation A
e:Equivalence eqA
exists l : list A,
  Permutation nil l /\ eqlistA eqA l nil
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:exists l : list A,
  Permutation l₁ l /\
  eqlistA eqA l l₂
exists l : list A,
  Permutation (x₁ :: l₁) l /\ eqlistA eqA l (x₂ :: l₂)
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
exists l0 : list A,
  Permutation (y :: x :: l) l0 /\
  eqlistA eqA l0 (x :: y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
IHPermutationA1:exists l : list A,
  Permutation l₁ l /\
  eqlistA eqA l l₂
IHPermutationA2:exists l : list A,
  Permutation l₂ l /\
  eqlistA eqA l l₃
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₃
 -
A:Type
eqA:relation A
e:Equivalence eqA
exists l : list A,
  Permutation nil l /\ eqlistA eqA l nil now exists nil.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:exists l : list A,
  Permutation l₁ l /\
  eqlistA eqA l l₂
exists l : list A,
  Permutation (x₁ :: l₁) l /\ eqlistA eqA l (x₂ :: l₂) destruct IHPermutationA as (l,(P,E)).
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
l:list A
P:Permutation l₁ l
E:eqlistA eqA l l₂
exists l0 : list A,
  Permutation (x₁ :: l₁) l0 /\
  eqlistA eqA l0 (x₂ :: l₂) exists (x₁::l); auto.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
exists l0 : list A,
  Permutation (y :: x :: l) l0 /\
  eqlistA eqA l0 (x :: y :: l) exists (x::y::l).
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
Permutation (y :: x :: l) (x :: y :: l) /\
eqlistA eqA (x :: y :: l) (x :: y :: l) split.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
Permutation (y :: x :: l) (x :: y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
eqlistA eqA (x :: y :: l) (x :: y :: l) constructor.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
eqlistA eqA (x :: y :: l) (x :: y :: l) reflexivity.
 -
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
IHPermutationA1:exists l : list A,
  Permutation l₁ l /\
  eqlistA eqA l l₂
IHPermutationA2:exists l : list A,
  Permutation l₂ l /\
  eqlistA eqA l l₃
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₃ destruct IHPermutationA1 as (l₁',(P,E)).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
IHPermutationA2:exists l : list A,
  Permutation l₂ l /\
  eqlistA eqA l l₃
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₃
   destruct IHPermutationA2 as (l₂',(P',E')).
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
l₂':list A
P':Permutation l₂ l₂'
E':eqlistA eqA l₂' l₃
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₃
   destruct (@Permutation_eqlistA_commute l₁' l₂ l₂') as (l₁'',(P'',E''));
    trivial.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
l₂':list A
P':Permutation l₂ l₂'
E':eqlistA eqA l₂' l₃
l₁'':list A
P'':Permutation l₁' l₁''
E'':eqlistA eqA l₁'' l₂'
exists l : list A,
  Permutation l₁ l /\ eqlistA eqA l l₃
   exists l₁''.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
l₂':list A
P':Permutation l₂ l₂'
E':eqlistA eqA l₂' l₃
l₁'':list A
P'':Permutation l₁' l₁''
E'':eqlistA eqA l₁'' l₂'
Permutation l₁ l₁'' /\ eqlistA eqA l₁'' l₃ split.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
l₂':list A
P':Permutation l₂ l₂'
E':eqlistA eqA l₂' l₃
l₁'':list A
P'':Permutation l₁' l₁''
E'':eqlistA eqA l₁'' l₂'
Permutation l₁ l₁''
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
l₂':list A
P':Permutation l₂ l₂'
E':eqlistA eqA l₂' l₃
l₁'':list A
P'':Permutation l₁' l₁''
E'':eqlistA eqA l₁'' l₂'
eqlistA eqA l₁'' l₃ now transitivity l₁'.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
l₁':list A
P:Permutation l₁ l₁'
E:eqlistA eqA l₁' l₂
l₂':list A
P':Permutation l₂ l₂'
E':eqlistA eqA l₂' l₃
l₁'':list A
P'':Permutation l₁' l₁''
E'':eqlistA eqA l₁'' l₂'
eqlistA eqA l₁'' l₃ now transitivity l₂'.
Qed.

Lemma Permutation_PermutationA l₁ l₂ :
 Permutation l₁ l₂ -> PermutationA l₁ l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
Permutation l₁ l₂ -> PermutationA l₁ l₂
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
Permutation l₁ l₂ -> PermutationA l₁ l₂
 induction 1.
A:Type
eqA:relation A
e:Equivalence eqA
PermutationA nil nil
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
H:Permutation l l'
IHPermutation:PermutationA l l'
PermutationA (x :: l) (x :: l')
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
PermutationA (y :: x :: l) (x :: y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:PermutationA l l'
IHPermutation2:PermutationA l' l''
PermutationA l l''
 -
A:Type
eqA:relation A
e:Equivalence eqA
PermutationA nil nil constructor.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x:A
l, l':list A
H:Permutation l l'
IHPermutation:PermutationA l l'
PermutationA (x :: l) (x :: l') now constructor.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
PermutationA (y :: x :: l) (x :: y :: l) apply permA_swap.
 -
A:Type
eqA:relation A
e:Equivalence eqA
l, l', l'':list A
H:Permutation l l'
H0:Permutation l' l''
IHPermutation1:PermutationA l l'
IHPermutation2:PermutationA l' l''
PermutationA l l'' econstructor; eauto.
Qed.

Lemma eqlistA_PermutationA l₁ l₂ :
 eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂
 induction 1; now constructor.
Qed.

Lemma NoDupA_equivlistA_decompose l1 l2 :
  NoDupA eqA l1 -> NoDupA eqA l2 -> equivlistA eqA l1 l2 ->
  exists l, Permutation l1 l /\ eqlistA eqA l l2.
A:Type
eqA:relation A
e:Equivalence eqA
l1, l2:list A
NoDupA eqA l1 ->
NoDupA eqA l2 ->
equivlistA eqA l1 l2 ->
exists l : list A,
  Permutation l1 l /\ eqlistA eqA l l2
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l1, l2:list A
NoDupA eqA l1 ->
NoDupA eqA l2 ->
equivlistA eqA l1 l2 ->
exists l : list A,
  Permutation l1 l /\ eqlistA eqA l l2
 intros.
A:Type
eqA:relation A
e:Equivalence eqA
l1, l2:list A
H:NoDupA eqA l1
H0:NoDupA eqA l2
H1:equivlistA eqA l1 l2
exists l : list A,
  Permutation l1 l /\ eqlistA eqA l l2 apply PermutationA_decompose.
A:Type
eqA:relation A
e:Equivalence eqA
l1, l2:list A
H:NoDupA eqA l1
H0:NoDupA eqA l2
H1:equivlistA eqA l1 l2
PermutationA l1 l2
 now apply NoDupA_equivlistA_PermutationA.
Qed.

Lemma PermutationA_preserves_NoDupA l₁ l₂ :
 PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂
Proof.
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂:list A
PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂
 induction 1; trivial.
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:NoDupA eqA l₁ -> NoDupA eqA l₂
NoDupA eqA (x₁ :: l₁) -> NoDupA eqA (x₂ :: l₂)
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
NoDupA eqA (y :: x :: l) -> NoDupA eqA (x :: y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
IHPermutationA1:NoDupA eqA l₁ -> NoDupA eqA l₂
IHPermutationA2:NoDupA eqA l₂ -> NoDupA eqA l₃
NoDupA eqA l₁ -> NoDupA eqA l₃
 -
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:NoDupA eqA l₁ -> NoDupA eqA l₂
NoDupA eqA (x₁ :: l₁) -> NoDupA eqA (x₂ :: l₂) inversion_clear 1; constructor; auto.
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:PermutationA l₁ l₂
IHPermutationA:NoDupA eqA l₁ -> NoDupA eqA l₂
H2:~ InA eqA x₁ l₁
H3:NoDupA eqA l₁
~ InA eqA x₂ l₂
   apply PermutationA_equivlistA in H0.
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:equivlistA eqA l₁ l₂
IHPermutationA:NoDupA eqA l₁ -> NoDupA eqA l₂
H2:~ InA eqA x₁ l₁
H3:NoDupA eqA l₁
~ InA eqA x₂ l₂ contradict H2.
A:Type
eqA:relation A
e:Equivalence eqA
x₁, x₂:A
l₁, l₂:list A
H:eqA x₁ x₂
H0:equivlistA eqA l₁ l₂
IHPermutationA:NoDupA eqA l₁ -> NoDupA eqA l₂
H3:NoDupA eqA l₁
H2:InA eqA x₂ l₂
InA eqA x₁ l₁
   now rewrite H, H0.
 -
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
NoDupA eqA (y :: x :: l) -> NoDupA eqA (x :: y :: l) inversion_clear 1.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H1:NoDupA eqA (x :: l)
NoDupA eqA (x :: y :: l) inversion_clear H1.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H:~ InA eqA x l
H2:NoDupA eqA l
NoDupA eqA (x :: y :: l) constructor.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H:~ InA eqA x l
H2:NoDupA eqA l
~ InA eqA x (y :: l)
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H:~ InA eqA x l
H2:NoDupA eqA l
NoDupA eqA (y :: l)
   +
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H:~ InA eqA x l
H2:NoDupA eqA l
~ InA eqA x (y :: l) contradict H.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H2:NoDupA eqA l
H:InA eqA x (y :: l)
InA eqA x l inversion_clear H; trivial.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H2:NoDupA eqA l
H1:eqA x y
InA eqA x l
     elim H0.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H2:NoDupA eqA l
H1:eqA x y
InA eqA y (x :: l) now constructor.
   +
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H:~ InA eqA x l
H2:NoDupA eqA l
NoDupA eqA (y :: l) constructor; trivial.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H0:~ InA eqA y (x :: l)
H:~ InA eqA x l
H2:NoDupA eqA l
~ InA eqA y l
     contradict H0.
A:Type
eqA:relation A
e:Equivalence eqA
x, y:A
l:list A
H:~ InA eqA x l
H2:NoDupA eqA l
H0:InA eqA y l
InA eqA y (x :: l) now apply InA_cons_tl.
 -
A:Type
eqA:relation A
e:Equivalence eqA
l₁, l₂, l₃:list A
H:PermutationA l₁ l₂
H0:PermutationA l₂ l₃
IHPermutationA1:NoDupA eqA l₁ -> NoDupA eqA l₂
IHPermutationA2:NoDupA eqA l₂ -> NoDupA eqA l₃
NoDupA eqA l₁ -> NoDupA eqA l₃ eauto.
Qed.

End Permutation.