Require Import Arith.
Require Import NArith.
Require Import List.
Require Import Sorting.
Require Import Coq.Program.Equality.

Lemma minus_n_0 : forall n, n-0 = n.
Proof.
(* Goal: forall n : nat, @eq nat (Init.Nat.add n (S O)) (S n) *)
induction n; trivial.
Defined.

Lemma plus_0_n : forall n, 0+n = n.
Proof.
(* Goal: forall n : nat, @eq nat (Init.Nat.add n (S O)) (S n) *)
induction n; trivial.
Defined.

Lemma plus_n_0 : forall n, n+0 = n.
Proof.
(* Goal: forall n : nat, @eq nat (Init.Nat.add n (S O)) (S n) *)
induction n; trivial.
(* Goal: @eq nat (Init.Nat.add (S n) (S O)) (S (S n)) *)
simpl; rewrite IHn; reflexivity.
Defined.

Lemma plus_n_1 : forall n, n+1 = S n.
Proof.
(* Goal: forall n : nat, @eq nat (Init.Nat.add n (S O)) (S n) *)
induction n; trivial.
(* Goal: @eq nat (Init.Nat.add (S n) (S O)) (S (S n)) *)
simpl; rewrite IHn; reflexivity.
Defined.

Lemma minus_n1_n2_0 : forall n1 n2, n1+n2-0 = n1+n2.
Proof.
(* Goal: forall n1 n2 : nat, @eq nat (Init.Nat.sub (Init.Nat.add n1 n2) O) (Init.Nat.add n1 n2) *)
induction n1; induction n2; trivial.
Defined.

Fixpoint arity (T:Type) (n:nat) :=
 match n with
 | 0 => Prop
 | S p => T -> arity T p
 end.

(* Warning cartesianPower T 0 represents T but it is never used *)

Fixpoint cartesianPowerAux (T:Type) (n:nat) :=
 match n with
 | 0 => T
 | S p => (T * cartesianPowerAux T p)%type
 end.

Definition cartesianPower T n := cartesianPowerAux T (n-1).

Definition headCP {T:Type} {n:nat} (cp : cartesianPower T (S n)) : T.
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPowerAux T n *)
exact cp.
(* Goal: cartesianPower T (S O) *)
exact (fst cp).
Defined.

Definition headCPbis {T:Type} {n:nat} (cp : cartesianPower T (S n)) : cartesianPower T 1.
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPowerAux T n *)
exact cp.
(* Goal: cartesianPower T (S O) *)
exact (fst cp).
Defined.

Definition tailCP {T:Type} {n:nat} (cp : cartesianPower T (S (S n))) : (cartesianPower T (S n)).
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPower T (S (S n)) *)
exact (snd cp).
(* Goal: cartesianPower T (S (S n)) *)
exact (snd cp).
Defined.

Definition tailDefaultCP {T:Type} {n:nat} (cp : cartesianPower T (S n)) (Default : cartesianPower T n) : (cartesianPower T n).
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPower T (@length T (@nil T)) *)
(* Goal: cartesianPower T (@length T (@cons T a l)) *)
exact Default.
(* Goal: cartesianPower T (S n) *)
exact (tailCP cp).
Defined.

Definition allButLastCP {T:Type} {n:nat} (cp : cartesianPower T (S (S n))) : (cartesianPower T (S n)).
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: T *)
exact (headCP cp).
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.
(* Goal: T *)
exact (headCP cp).
(* Goal: cartesianPowerAux T n *)
unfold cartesianPower in IHn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
simpl in *.
(* Goal: cartesianPowerAux T n *)
rewrite minus_n_0 in IHn.
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n cp1) (@tailCP T n cp2) *)
apply IHn.
(* Goal: cartesianPower T (S n) *)
exact (tailCP cp).
Defined.

Lemma allButLastCPTl {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S (S n)))),
  allButLastCP (tailCP cp) = tailCP (allButLastCP cp).
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t : T), @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) cp t)) (@consTailCP T (S n) (@tailCP T n cp) t) *)
intro cp; induction n; simpl; reflexivity.
Qed.

Definition lastCP {T:Type} {n:nat} (cp : cartesianPower T (S n)) : T.
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPowerAux T n *)
exact cp.
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n cp1) (@tailCP T n cp2) *)
apply IHn.
(* Goal: cartesianPower T (S n) *)
exact (tailCP cp).
Defined.

Lemma lastCPTl {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))), lastCP cp = lastCP (tailCP cp).
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t : T), @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) cp t)) (@consTailCP T (S n) (@tailCP T n cp) t) *)
intro cp; induction n; simpl; reflexivity.
Qed.

Lemma CP_ind {T:Type} {n : nat} : forall (cp cp' : cartesianPower T (S (S n))),
  headCP cp = headCP cp' -> tailCP cp = tailCP cp' -> cp = cp'.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
induction n; simpl in *;
(* Goal: @NoDup A (@cons A a l) *)
apply injective_projections; assumption.
Qed.

Definition CPPair {T : Type} :
  forall (cp : cartesianPower T 2),
  cp = (fst cp, snd cp).
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: @eq (cartesianPower T (S (S O))) cp (@pair T T (@fst T T cp) (@snd T T cp)) *)
apply CP_ind; simpl; reflexivity.
Qed.

Definition tailCPbis {T:Type} {n:nat} m1 m2 (cp : cartesianPower T m1) :
  (S (S n)) = m1 -> (S n) = m2 -> (cartesianPower T m2).
Proof.
(* Goal: forall (_ : @eq nat (S (S n)) m1) (_ : @eq nat (S n) m2), cartesianPower T m2 *)
intros Hm1 Hm2.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
subst.
(* Goal: cartesianPower T (S n) *)
exact (tailCP cp).
Defined.

Definition consHeadCP {T:Type} {n:nat} (t : T) (cp : cartesianPower T n) : (cartesianPower T (S n)).
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPower T (S O) *)
(* Goal: cartesianPower T (S (S n)) *)
exact t.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
clear IHn.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.
(* Goal: cartesianPower T (S O) *)
(* Goal: cartesianPower T (S (S n)) *)
exact t.
(* Goal: cartesianPowerAux T n *)
unfold cartesianPower in cp.
(* Goal: cartesianPowerAux T n *)
simpl in cp.
(* Goal: cartesianPowerAux T n *)
rewrite minus_n_0 in cp.
(* Goal: cartesianPowerAux T n *)
exact cp.
Defined.

Lemma consHeadCPHd {T:Type} {n:nat} :
  forall (cp : cartesianPower T n) t,
  headCP (consHeadCP t cp) = t.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t : T), @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) cp t)) (@consTailCP T (S n) (@tailCP T n cp) t) *)
intro cp; induction n; simpl; reflexivity.
Qed.

Lemma consHeadCPTl {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) t,
  tailCP (consHeadCP t cp) = cp.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t : T), @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) cp t)) (@consTailCP T (S n) (@tailCP T n cp) t) *)
intro cp; induction n; simpl; reflexivity.
Qed.

Lemma consHeadCPOK {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))),
  cp = consHeadCP (headCP cp) (tailCP cp).
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: @eq (cartesianPower T (S (S O))) cp (@pair (cartesianPower T (S O)) T (@fst T T cp) (@snd T T cp)) *)
(* Goal: @eq (cartesianPower T (S (S (S n)))) cp (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp) (@lastCP T (S (S n)) cp)) *)
apply CPPair.
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S (S n)))) (@consTailCP T (S (S n)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S (S n)) X) (@tailCP T (S n) X))) C) (@consTailCP T (S (S n)) (@tailCP T (S n) X) C) *)
rewrite consHeadCPTl; reflexivity.
Qed.

Definition consTailCP {T:Type} {n:nat} (cp : cartesianPower T n) (t : T) : (cartesianPower T (S n)).
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPower T (S O) *)
(* Goal: cartesianPower T (S (S n)) *)
exact t.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: cartesianPower T (S (S O)) *)
(* Goal: cartesianPower T (S (S (S n))) *)
exact (cp, t).
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
clear IHn0.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.
(* Goal: T *)
exact (headCP cp).
(* Goal: cartesianPowerAux T (S n) *)
exact (IHn (tailCP cp)).
Defined.

Lemma consTailCPTl {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) t,
  tailCP (consTailCP cp t) = consTailCP (tailCP cp) t.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t : T), @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) cp t)) (@consTailCP T (S n) (@tailCP T n cp) t) *)
intro cp; induction n; simpl; reflexivity.
Qed.

Lemma consTailCPOK {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))),
  cp = consTailCP (allButLastCP cp) (lastCP cp).
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: @eq (cartesianPower T (S (S O))) cp (@pair (cartesianPower T (S O)) T (@fst T T cp) (@snd T T cp)) *)
(* Goal: @eq (cartesianPower T (S (S (S n)))) cp (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp) (@lastCP T (S (S n)) cp)) *)
apply CPPair.
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (@lastCP T n (@tailCP T n cp))) (@In T (@lastCP T n (@tailCP T n cp)) (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n cp))) *)
assert (H := IHn (tailCP cp)).
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) cp) (@tailCP T (S n) (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp) (@lastCP T (S (S n)) cp))) *)
rewrite <- lastCPTl in H.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) cp) (@tailCP T (S n) (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp) (@lastCP T (S (S n)) cp))) *)
rewrite allButLastCPTl in H.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) cp) (@tailCP T (S n) (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp) (@lastCP T (S (S n)) cp))) *)
rewrite <- consTailCPTl in H.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
Qed.

Lemma consTailCPAbl {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) t,
  allButLastCP (consTailCP cp t) = cp.
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (t : T), @eq T (@lastCP T (S n) (@consTailCP T (S n) cp t)) t *)
intros cp t; induction n; try (simpl; reflexivity).
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S m))) (@circPermNCP T m n (@consTailCP T (S m) (@tailCP T m (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) (@headCP T (S m) (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))))) (@consTailCP T (S m) (@tailCP T m (@circPermNCP T m (S n) cp)) (@headCP T (S m) (@circPermNCP T m (S n) cp))) *)
rewrite <- IHn.
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n (@allButLastCP T (S n) (@consTailCP T (S (S n)) cp t))) (@allButLastCP T n (@consTailCP T (S n) (@tailCP T n cp) t)) *)
rewrite <- consTailCPTl.
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n (@allButLastCP T (S n) (@consTailCP T (S (S n)) cp t))) (@allButLastCP T n (@tailCP T (S n) (@consTailCP T (S (S n)) cp t))) *)
rewrite allButLastCPTl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma consTailCPTlD {T:Type} {n:nat} :
  forall (cp : cartesianPower T n) t,
  tailDefaultCP (consHeadCP t cp) cp = cp.
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (t : T), @eq T (@lastCP T (S n) (@consTailCP T (S n) cp t)) t *)
intros cp t; induction n; try (simpl; reflexivity).
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
induction n; simpl; reflexivity.
Qed.

Lemma consHdTlTlHd {T:Type} {n:nat} :
  forall (F L : T) (X : cartesianPower T n),
  consHeadCP F (consTailCP X L) = consTailCP (consHeadCP F X) L.
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: forall (F L : T) (X : cartesianPower T (S (S n))), @eq (cartesianPower T (S (S (S (S n))))) (@consHeadCP T (S (S (S n))) F (@consTailCP T (S (S n)) X L)) (@consTailCP T (S (S (S n))) (@consHeadCP T (S (S n)) F X) L) *)
intros F L X.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
unfold consHeadCP; unfold consTailCP; simpl; reflexivity.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
clear IHn.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: forall (F L : T) (X : cartesianPower T (S (S n))), @eq (cartesianPower T (S (S (S (S n))))) (@consHeadCP T (S (S (S n))) F (@consTailCP T (S (S n)) X L)) (@consTailCP T (S (S (S n))) (@consHeadCP T (S (S n)) F X) L) *)
intros F L X.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
unfold consHeadCP; unfold consTailCP; simpl; reflexivity.
(* Goal: forall (F L : T) (X : cartesianPower T (S (S n))), @eq (cartesianPower T (S (S (S (S n))))) (@consHeadCP T (S (S (S n))) F (@consTailCP T (S (S n)) X L)) (@consTailCP T (S (S (S n))) (@consHeadCP T (S (S n)) F X) L) *)
intros F L X.
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@tailCP T (S (S (S n))) (@consHeadCP T (S (S (S (S n)))) A (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) X C)))) (@tailCP T (S (S (S n))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) A (@consHeadCP T (S (S n)) B X)) C)) *)
assert (H := consHeadCPOK X); rewrite H; clear H.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S n) X) (@consTailCP T (S n) (@tailCP T n X) C))) *)
rewrite consHeadCPTl.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@consTailCP T (S n) (@tailCP T n X) C) *)
rewrite consTailCPTl.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S n) X) (@consTailCP T (S n) (@tailCP T n X) C))) *)
rewrite consHeadCPTl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma consTlHdHdTl {T:Type} {n:nat} :
  forall (A B C : T) (X : cartesianPower T n),
  consHeadCP A (consHeadCP B (consTailCP X C)) = consTailCP (consHeadCP A (consHeadCP B X)) C.
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: forall (A B C : T) (X : cartesianPower T (S (S n))), @eq (cartesianPower T (S (S (S (S (S n)))))) (@consHeadCP T (S (S (S (S n)))) A (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) X C))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) A (@consHeadCP T (S (S n)) B X)) C) *)
intros A B C X.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
unfold consHeadCP; unfold consTailCP; simpl; reflexivity.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
clear IHn.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: forall (A B C : T) (X : cartesianPower T (S (S n))), @eq (cartesianPower T (S (S (S (S (S n)))))) (@consHeadCP T (S (S (S (S n)))) A (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) X C))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) A (@consHeadCP T (S (S n)) B X)) C) *)
intros A B C X.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
unfold consHeadCP; unfold consTailCP; simpl; reflexivity.
(* Goal: forall (A B C : T) (X : cartesianPower T (S (S n))), @eq (cartesianPower T (S (S (S (S (S n)))))) (@consHeadCP T (S (S (S (S n)))) A (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) X C))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) A (@consHeadCP T (S (S n)) B X)) C) *)
intros A B C X.
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@tailCP T (S (S (S n))) (@consHeadCP T (S (S (S (S n)))) A (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) X C)))) (@tailCP T (S (S (S n))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) A (@consHeadCP T (S (S n)) B X)) C)) *)
assert (H := consHeadCPOK X); rewrite H; clear H.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S n) X) (@consTailCP T (S n) (@tailCP T n X) C))) *)
rewrite consHeadCPTl.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@consTailCP T (S n) (@tailCP T n X) C) *)
rewrite consTailCPTl.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S n) X) (@consTailCP T (S n) (@tailCP T n X) C))) *)
rewrite consHeadCPTl.
(* Goal: @eq (cartesianPower T (S (S m))) (@circPermNCP T m n (@consTailCP T (S m) (@tailCP T m (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) (@headCP T (S m) (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))))) (@consTailCP T (S m) (@tailCP T m (@circPermNCP T m (S n) cp)) (@headCP T (S m) (@circPermNCP T m (S n) cp))) *)
rewrite <- IHn.
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S (S n)))) (@tailCP T (S (S n)) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C))) (@tailCP T (S (S n)) (@consHeadCP T (S (S (S n))) B (@consHeadCP T (S (S n)) (@headCP T (S n) X) (@consTailCP T (S n) (@tailCP T n X) C)))) *)
do 2 (rewrite consHeadCPTl).
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S n) X) (@consTailCP T (S n) (@tailCP T n X) C))) *)
rewrite consHeadCPTl.
(* Goal: @eq (cartesianPower T (S (S n))) (@tailCP T (S n) (@consTailCP T (S (S n)) (@consHeadCP T (S n) (@headCP T (S n) X) (@tailCP T n X)) C)) (@consTailCP T (S n) (@tailCP T n X) C) *)
rewrite consTailCPTl.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S (S n)))) (@consTailCP T (S (S n)) (@tailCP T (S n) (@consHeadCP T (S (S n)) (@headCP T (S (S n)) X) (@tailCP T (S n) X))) C) (@consTailCP T (S (S n)) (@tailCP T (S n) X) C) *)
rewrite consHeadCPTl; reflexivity.
Qed.

Definition CPToList {T:Type} {n:nat} (cp : cartesianPower T n) : list T.
Proof.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: list T *)
(* Goal: list T *)
exact nil.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
clear IHn.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: list T *)
(* Goal: list T *)
exact (cons cp nil).
(* Goal: list T *)
apply cons.
(* Goal: T *)
exact (headCP cp).
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n cp1) (@tailCP T n cp2) *)
apply IHn.
(* Goal: cartesianPower T (S n) *)
exact (tailCP cp).
Defined.

Definition InCP {T:Type} {n:nat} p (cp : cartesianPower T n) := In p (CPToList cp).

Lemma InCPOK {T:Type} {n:nat} : forall p (cp : cartesianPower T (S (S n))),
  InCP p cp <-> ((p = headCP cp) \/ InCP p (tailCP cp)).
Proof.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
intros p cp; unfold InCP; induction n; simpl.

(* Goal: iff (or (@eq T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) p) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)))))) (or (@eq T p (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)))))) *)
  split; intro H.

(* Goal: or (@eq T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) p) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp))))) *)
    elim H; clear H; intro H.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
      left; subst; reflexivity.

(* Goal: @NoDup A (@cons A a l) *)
      right; assumption.

(* Goal: or (@eq T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) p) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp))))) *)
    elim H; clear H; intro H.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
      left; subst; reflexivity.

(* Goal: @NoDup A (@cons A a l) *)
      right; assumption.

(* Goal: iff (or (@eq T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) p) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)))))) (or (@eq T p (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)))))) *)
  split; intro H.

(* Goal: or (@eq T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) p) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp))))) *)
    elim H; clear H; intro H.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
      left; subst; reflexivity.

(* Goal: @NoDup A (@cons A a l) *)
      right; assumption.

(* Goal: or (@eq T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) p) (or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp)) p) (@In T p (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp))))) *)
    elim H; clear H; intro H.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
      left; subst; reflexivity.

(* Goal: @NoDup A (@cons A a l) *)
      right; assumption.
Qed.

Lemma lastCPIn {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)), InCP (lastCP cp) cp.
Proof.
(* Goal: forall cp : cartesianPower T (S n), @InCP T (S n) (@lastCP T n cp) cp *)
unfold InCP.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
intro cp; induction n.
(* Goal: @In T (@lastCP T O cp) (@CPToList T (S O) cp) *)
(* Goal: @In T (@lastCP T (S n) cp) (@CPToList T (S (S n)) cp) *)
simpl; intuition.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: or (@eq T (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (@lastCP T n (@tailCP T n cp))) (@In T (@lastCP T n (@tailCP T n cp)) (nat_rect (fun n : nat => forall _ : cartesianPower T (S n), list T) (fun cp : cartesianPower T (S O) => @cons (cartesianPower T (S O)) cp (@nil (cartesianPower T (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower T (S n), list T) (cp : cartesianPower T (S (S n))) => @cons T (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp) (IHn (@tailCP T n cp))) n (@tailCP T n cp))) *)
assert (H := IHn (tailCP cp)).
(* Goal: ge (S id) (S O) *)
intuition.
Qed.

Definition nthCP {T:Type} {m:nat} (n : nat) (cp : cartesianPower T m) (Default : T) := nth (n-1) (CPToList cp) Default.

Lemma CPToListOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))), CPToList cp = cons (headCP cp) (CPToList (tailCP cp)).
Proof.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma CPLHdTlOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))),
  CPToList cp = ((headCP cp) :: nil) ++ CPToList (tailCP cp).
Proof.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
induction n; intro cp; simpl; reflexivity.
Qed.

Lemma consTailOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) t,
  CPToList (consTailCP cp t) = CPToList cp ++ t :: nil.
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (t : T), @eq (list T) (@CPToList T (S (S n)) (@consTailCP T (S n) cp t)) (@app T (@CPToList T (S n) cp) (@cons T t (@nil T))) *)
induction n; intros cp t.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S id) (S O)) (@CPToList T (S (S n)) cp) Default) *)
rewrite CPToListOK.
(* Goal: @eq (list T) (@cons T (@headCP T (S (S n)) (@consTailCP T (S (S n)) cp t)) (@CPToList T (S (S n)) (@tailCP T (S n) (@consTailCP T (S (S n)) cp t)))) (@app T (@CPToList T (S (S n)) cp) (@cons T t (@nil T))) *)
assert (H : headCP (consTailCP cp t) = headCP cp) by (simpl; reflexivity); rewrite H; clear H.
assert (H : tailCP (consTailCP cp t) = (consTailCP (tailCP cp) t)) by (simpl; reflexivity);
(* Goal: @NoDup A l *)
rewrite H; clear H.
(* Goal: @eq (list T) (@cons T (@headCP T (S n) cp) (@CPToList T (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) t))) (@app T (@CPToList T (S (S n)) cp) (@cons T t (@nil T))) *)
rewrite IHn.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
Qed.

Lemma InNth {T:Type} {n:nat} :
  forall (cp : cartesianPower T n) (t Default : T),
  InCP t cp -> (exists id, id >= 1 /\ id <= n /\ t = nthCP id cp Default).
Proof.
(* Goal: forall (cp : cartesianPower T n) (t Default : T) (_ : @InCP T n t cp), @ex nat (fun id : nat => and (ge id (S O)) (and (le id n) (@eq T t (@nthCP T n id cp Default)))) *)
induction n; intros cp t Default HIn.
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id O) (@eq T t (@nthCP T O id cp Default)))) *)
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S n)) (@eq T t (@nthCP T (S n) id cp Default)))) *)
unfold InCP in HIn.
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id O) (@eq T t (@nthCP T O id cp Default)))) *)
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S n)) (@eq T t (@nthCP T (S n) id cp Default)))) *)
simpl in HIn.
(* Goal: ge (S id) (S O) *)
intuition.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: ge (S id) (S O) *)
exists 1; try intuition.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
unfold nthCP; simpl.
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id O) (@eq T t (@nthCP T O id cp Default)))) *)
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S n)) (@eq T t (@nthCP T (S n) id cp Default)))) *)
unfold InCP in HIn; simpl in HIn.
(* Goal: ge (S id) (S O) *)
intuition.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
clear IHn0.
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S (S n))) (@eq T t (@nthCP T (S (S n)) id cp Default)))) *)
apply InCPOK in HIn.
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
elim HIn; clear HIn; intro HIn.
(* Goal: @In T (@lastCP T O cp) (@CPToList T (S O) cp) *)
(* Goal: @In T (@lastCP T (S n) cp) (@CPToList T (S (S n)) cp) *)
exists 1; unfold nthCP; simpl; intuition.
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S (S n))) (@eq T t (@nthCP T (S (S n)) id cp Default)))) *)
assert (H := IHn (tailCP cp) t Default).
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S (S n))) (@eq T t (@nthCP T (S (S n)) id cp Default)))) *)
apply H in HIn; clear H.
(* Goal: @ex nat (fun id : nat => and (ge id (S O)) (and (le id (S (S n))) (@eq T t (@nthCP T (S (S n)) id cp Default)))) *)
destruct HIn as [id [Hge [Hle HEq]]].
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
unfold nthCP in *.
(* Goal: ge (S id) (S O) *)
exists (S id); try intuition.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S id) (S O)) (@CPToList T (S (S n)) cp) Default) *)
assert (H := app_nth2 ((headCP cp) :: nil) (CPToList (tailCP cp)) Default Hge).
(* Goal: @eq T t (@nth T (Init.Nat.sub (S id) (S O)) (@CPToList T (S (S n)) cp) Default) *)
rewrite CPToListOK.
assert (H' : (headCP cp :: nil) ++ CPToList (tailCP cp) = (headCP cp :: CPToList (tailCP cp)))
  by (simpl; reflexivity); rewrite <- H'; clear H'.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S id) (S O)) (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) Default) *)
assert (H' : (S id - 1) = id) by (simpl; rewrite minus_n_0; reflexivity); rewrite H'; clear H'.
(* Goal: @eq T t (@nth T id (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) Default) *)
rewrite H.
(* Goal: @eq T t (@nth T (Init.Nat.sub id (@length T (@cons T (@headCP T (S n) cp) (@nil T)))) (@CPToList T (S n) (@tailCP T n cp)) Default) *)
apply HEq.
Qed.

Lemma nthFirst {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) (t Default : T),
  t = nthCP 1 cp Default -> t = headCP cp.
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (t Default : T) (_ : @eq T t (@nthCP T (S n) (S O) cp Default)), @eq T t (@headCP T n cp) *)
induction n; intros cp t Default Hnth.
(* Goal: @eq T t (@headCP T (S n) cp) *)
unfold nthCP in Hnth.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S (S O)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp))) Default) *)
(* Goal: @eq T t (@nthCP T (S (S O)) (S (S id)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp)) Default) *)
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
simpl in Hnth.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
(* Goal: @eq T t (@headCP T (S n) cp) *)
unfold nthCP in Hnth.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S (S O)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp))) Default) *)
(* Goal: @eq T t (@nthCP T (S (S O)) (S (S id)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp)) Default) *)
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
simpl in Hnth.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
Qed.

Lemma lengthOfCPToList {T:Type} {n:nat} : forall (cp : cartesianPower T n), n = length (CPToList cp).
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
clear IHn.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
(* Goal: @eq nat (S (S n)) (@length T (@CPToList T (S (S n)) cp)) *)
apply eq_S.
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n cp1) (@tailCP T n cp2) *)
apply IHn.
Defined.

Lemma lastTailOK {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))),
  lastCP cp = lastCP (tailCP cp).
Proof.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
induction n; intro cp; simpl; reflexivity.
Qed.

Lemma consTailCPLast {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) t,
  lastCP (consTailCP cp t) = t.
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (t : T), @eq T (@lastCP T (S n) (@consTailCP T (S n) cp t)) t *)
intros cp t; induction n; try (simpl; reflexivity).
(* Goal: @eq T (@lastCP T (S n) cp) (@nth T (Init.Nat.sub (S (S n)) (S O)) (@CPToList T (S (S n)) cp) Default) *)
rewrite lastTailOK.
(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n cp1) (@tailCP T n cp2) *)
apply IHn.
Qed.

Lemma nthLast {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) (Default : T),
  lastCP cp = nthCP (S n) cp Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (Default : T), @eq T (@lastCP T n cp) (@nthCP T (S n) (S n) cp Default) *)
unfold nthCP; induction n; intros cp Default.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq T (@lastCP T (S n) cp) (@nth T (Init.Nat.sub (S (S n)) (S O)) (@CPToList T (S (S n)) cp) Default) *)
rewrite lastTailOK.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
assert (H := IHn (tailCP cp) Default); rewrite H; clear H; clear IHn.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: le (S (S n)) (Init.Nat.sub m O) *)
rewrite minus_n_0.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma nthCircPerm1 {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) (t Default : T),
  t = nthCP 1 cp Default -> t = nthCP (S (S n)) (consTailCP (tailCP cp) (headCP cp)) Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t Default : T) (_ : @eq T t (@nthCP T (S (S n)) (S O) cp Default)), @eq T t (@nthCP T (S (S n)) (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) *)
intros cp t Default Hnth.
(* Goal: @eq T t (@nthCP T (S (S n)) (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) *)
apply nthFirst in Hnth.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S (S O)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp))) Default) *)
(* Goal: @eq T t (@nthCP T (S (S O)) (S (S id)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp)) Default) *)
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
rewrite <- Hnth.
(* Goal: @eq T t (@nthCP T (S (S n)) (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) t) Default) *)
clear Hnth.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
unfold nthCP.
(* Goal: @Permutation.Permutation T (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) (@CPToList T (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) *)
rewrite consTailOK.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S (S n)) (S O)) (@app T (@CPToList T (S n) (@tailCP T n cp)) (@cons T t (@nil T))) Default) *)
rewrite app_nth2.
(* Goal: le (@length T (@CPToList T (S (S n)) cp)) (Init.Nat.sub (S m) (S O)) *)
rewrite <- lengthOfCPToList.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: @eq T t match Init.Nat.sub n n with | O => t | S (O as m) => Default | S (S m0 as m) => Default end *)
(* Goal: ge (Init.Nat.sub (S (S n)) (S O)) (@length T (@CPToList T (S n) (@tailCP T n cp))) *)
rewrite <- Minus.minus_diag_reverse.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
(* Goal: le (@length T (@CPToList T (S (S n)) cp)) (Init.Nat.sub (S m) (S O)) *)
rewrite <- lengthOfCPToList.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: ge (S id) (S O) *)
intuition.
Qed.

Lemma nthCircPerm1Eq {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) (Default : T),
  nthCP 1 cp Default = nthCP (S (S n)) (consTailCP (tailCP cp) (headCP cp)) Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (_ : T), @eq (cartesianPower T (S (S n))) cp (@circPermNCP T n (S (S n)) cp) *)
intros cp Default.
(* Goal: @eq T (@nthCP T (S (S n)) (S O) cp Default) (@nthCP T (S (S n)) (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) *)
apply nthCircPerm1.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma nthCircPerm2 {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) (t Default : T) id,
  t = nthCP (S (S id)) cp Default -> id <= n ->
  t = nthCP (S id) (consTailCP (tailCP cp) (headCP cp)) Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (t Default : T) (id : nat) (_ : @eq T t (@nthCP T (S (S n)) (S (S id)) cp Default)) (_ : le id n), @eq T t (@nthCP T (S (S n)) (S id) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) *)
induction n; intros cp t Default id Hnth HIn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
simpl in *.
(* Goal: @eq T t (@nthCP T (S (S O)) (S id) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp)) Default) *)
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
induction id.
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
unfold nthCP in *.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S (S O)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp))) Default) *)
(* Goal: @eq T t (@nthCP T (S (S O)) (S (S id)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp)) Default) *)
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
simpl in Hnth.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S (S O)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp))) Default) *)
(* Goal: @eq T t (@nthCP T (S (S O)) (S (S id)) (@pair (cartesianPower T (S O)) T (@snd T T cp) (@fst T T cp)) Default) *)
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
rewrite <- Hnth.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: ge (S id) (S O) *)
assert (H := Le.le_Sn_0 id); intuition.
(* Goal: @eq T t (@nthCP T (S (S (S n))) (S id) (@consTailCP T (S (S n)) (@tailCP T (S n) cp) (@headCP T (S (S n)) cp)) Default) *)
unfold nthCP in *.
(* Goal: @Permutation.Permutation T (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) (@CPToList T (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) *)
rewrite consTailOK.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S id) (S O)) (@app T (@CPToList T (S (S n)) (@tailCP T (S n) cp)) (@cons T (@headCP T (S (S n)) cp) (@nil T))) Default) *)
rewrite CPLHdTlOK in Hnth.
(* Goal: @eq T t (@nth T (Init.Nat.sub (S id) (S O)) (@app T (@CPToList T (S (S n)) (@tailCP T (S n) cp)) (@cons T (@headCP T (S (S n)) cp) (@nil T))) Default) *)
rewrite app_nth2 in Hnth.
assert (H : S (S id) - 1 - length (headCP cp :: nil)  = S id - 1) by (simpl; reflexivity);
(* Goal: @NoDup A l *)
rewrite H in Hnth; clear H.
(* Goal: @NoDup A (@cons A a l) *)
rewrite app_nth1; try assumption.
(* Goal: le (@length T (@CPToList T (S (S n)) cp)) (Init.Nat.sub (S m) (S O)) *)
rewrite <- lengthOfCPToList.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: le (S (S n)) (Init.Nat.sub m O) *)
rewrite minus_n_0.
(* Goal: @NoDup A (@cons A a l) *)
apply Lt.le_lt_n_Sm; assumption.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: ge (S id) (S O) *)
intuition.
Qed.

Lemma nthCircPerm2Eq {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) (Default : T) id,
  id <= n -> nthCP (S (S id)) cp Default = nthCP (S id) (consTailCP (tailCP cp) (headCP cp)) Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (Default : T) (id : nat) (_ : le id n), @eq T (@nthCP T (S (S n)) (S (S id)) cp Default) (@nthCP T (S (S n)) (S id) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) *)
intros cp Default id Hle.
(* Goal: @eq T (@nthCP T (S (S n)) (S (S id)) cp Default) (@nthCP T (S (S n)) (S id) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) *)
apply nthCircPerm2.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
Qed.

Lemma nthCPTlOK {T:Type} {m:nat} :
  forall (cp : cartesianPower T (S (S m))) (Default : T) n,
  nthCP (S n) (tailCP cp) Default = nthCP (S (S n)) cp Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S m))) (Default : T) (n : nat), @eq T (@nthCP T (S m) (S n) (@tailCP T m cp) Default) (@nthCP T (S (S m)) (S (S n)) cp Default) *)
induction m; intros cp Default n.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
induction n; unfold nthCP; simpl; reflexivity.
(* Goal: @eq T (@nthCP T (S (S m)) (S n) (@tailCP T (S m) cp) Default) (@nthCP T (S (S (S m))) (S (S n)) cp Default) *)
assert (H := nthCircPerm2 cp (nthCP (S (S n)) cp Default) Default n).
(* Goal: @eq T (@nthCP T (S (S m)) (S n) (@tailCP T (S m) cp) Default) (@nthCP T (S (S (S m))) (S (S n)) cp Default) *)
assert (Hnm := le_lt_dec n (S m)).
(* Goal: @eq T (@nthCP T (S (S m)) (S n) (@tailCP T (S m) cp) Default) (@nthCP T (S (S (S m))) (S (S n)) cp Default) *)
elim Hnm; clear Hnm; intro Hnm.
assert (H' : nthCP (S (S n)) cp Default = nthCP (S (S n)) cp Default) by reflexivity; apply H in H'; try assumption;
clear H; rewrite H'; clear H'.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
unfold nthCP.
(* Goal: @Permutation.Permutation T (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) (@CPToList T (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) *)
rewrite consTailOK.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
rewrite app_nth1; try reflexivity.
(* Goal: le (@length T (@CPToList T (S (S n)) cp)) (Init.Nat.sub (S m) (S O)) *)
rewrite <- lengthOfCPToList.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: le (S (S n)) (Init.Nat.sub m O) *)
rewrite minus_n_0.
(* Goal: @NoDup A (@cons A a l) *)
apply Lt.le_lt_n_Sm; assumption.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
unfold nthCP.
(* Goal: @eq T (@nth T (Init.Nat.sub (S m) (S O)) (@CPToList T (S (S n)) cp) Default) (@nth T (Init.Nat.sub (S m) (S O)) (@CPToList T (S (S n)) (@circPermNCP T n (S (S n)) cp)) Default) *)
rewrite nth_overflow.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
rewrite nth_overflow; try reflexivity.
(* Goal: @In T (@lastCP T O cp) (@CPToList T (S O) cp) *)
(* Goal: @In T (@lastCP T (S n) cp) (@CPToList T (S (S n)) cp) *)
rewrite <- lengthOfCPToList; simpl; intuition.
(* Goal: ge (S id) (S O) *)
rewrite <- lengthOfCPToList; simpl; rewrite minus_n_0; intuition.
Qed.

Lemma nthEqOK {T:Type} {m:nat} :
  forall (cp1 cp2 : cartesianPower T (S m)) (Default : T),
  (forall n, nthCP n cp1 Default = nthCP n cp2 Default) -> cp1 = cp2.
Proof.
(* Goal: forall (cp1 cp2 : cartesianPower T (S m)) (Default : T) (_ : forall n : nat, @eq T (@nthCP T (S m) n cp1 Default) (@nthCP T (S m) n cp2 Default)), @eq (cartesianPower T (S m)) cp1 cp2 *)
induction m; intros cp1 cp2 Default Hnth.
(* Goal: @eq T (@headCP T (S m) cp1) (@headCP T (S m) cp2) *)
(* Goal: @eq (cartesianPower T (S m)) (@tailCP T m cp1) (@tailCP T m cp2) *)
assert (H := Hnth 1).
(* Goal: @eq T (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp1)) Default) (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp2)) Default) *)
(* Goal: @eq T (@nthCP T (S m) (S n) (@tailCP T m cp1) Default) (@nthCP T (S m) (S n) (@tailCP T m cp2) Default) *)
unfold nthCP in H.
(* Goal: @NoDup A l *)
simpl in H.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
apply CP_ind.
(* Goal: @eq T (@headCP T (S m) cp1) (@headCP T (S m) cp2) *)
(* Goal: @eq (cartesianPower T (S m)) (@tailCP T m cp1) (@tailCP T m cp2) *)
assert (H := Hnth 1).
(* Goal: @eq T (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp1)) Default) (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp2)) Default) *)
(* Goal: @eq T (@nthCP T (S m) (S n) (@tailCP T m cp1) Default) (@nthCP T (S m) (S n) (@tailCP T m cp2) Default) *)
unfold nthCP in H.
(* Goal: @NoDup A l *)
simpl in H.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
(* Goal: @eq (cartesianPower T (S m)) (@tailCP T m cp1) (@tailCP T m cp2) *)
apply IHm with Default.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
intro n; induction n.
(* Goal: @eq T (@nthCP T (S m) O (@tailCP T m cp1) Default) (@nthCP T (S m) O (@tailCP T m cp2) Default) *)
(* Goal: @eq T (@nthCP T (S m) (S n) (@tailCP T m cp1) Default) (@nthCP T (S m) (S n) (@tailCP T m cp2) Default) *)
assert (H := Hnth 2).
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
unfold nthCP.
(* Goal: @eq T (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp1)) Default) (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp2)) Default) *)
(* Goal: @eq T (@nthCP T (S m) (S n) (@tailCP T m cp1) Default) (@nthCP T (S m) (S n) (@tailCP T m cp2) Default) *)
unfold nthCP in H.
(* Goal: @eq T (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp1)) Default) (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S m) (@tailCP T m cp2)) Default) *)
(* Goal: @eq T (@nthCP T (S m) (S n) (@tailCP T m cp1) Default) (@nthCP T (S m) (S n) (@tailCP T m cp2) Default) *)
do 2 (rewrite CPLHdTlOK in H).
(* Goal: @NoDup A (@cons A a l) *)
simpl; assumption.
(* Goal: @eq T (@nthCP T (S m) (S n) (@tailCP T m cp1) Default) (@nthCP T (S m) (S n) (@tailCP T m cp2) Default) *)
do 2 (rewrite nthCPTlOK).
(* Goal: @eq T (@nthCP T (S (S m)) (S (S n)) cp1 Default) (@nthCP T (S (S m)) (S (S n)) cp2 Default) *)
apply Hnth.
Qed.

Lemma consTailPerm  {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))),
  Permutation.Permutation (CPToList cp) (CPToList (consTailCP (tailCP cp) (headCP cp))).
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: @Permutation.Permutation T (@CPToList T (S (S n)) cp) (@CPToList T (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) *)
rewrite CPLHdTlOK.
(* Goal: @Permutation.Permutation T (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) (@CPToList T (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) *)
rewrite consTailOK.
(* Goal: @Permutation.Permutation T (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) (@app T (@CPToList T (S n) (@tailCP T n cp)) (@cons T (@headCP T (S n) cp) (@nil T))) *)
apply Permutation.Permutation_app_comm.
Qed.

Definition ListToCP {T : Type} (l : list T) (Default : T) : cartesianPower T (length l).
Proof.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.
(* Goal: cartesianPower T (@length T (@nil T)) *)
(* Goal: cartesianPower T (@length T (@cons T a l)) *)
exact Default.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.
(* Goal: T *)
(* Goal: cartesianPowerAux T (@length T l) *)
exact a.
(* Goal: cartesianPower T (@length T (@cons T a (@cons T a0 l))) *)
clear IHl0.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.
(* Goal: T *)
(* Goal: cartesianPowerAux T (@length T l) *)
exact a.
(* Goal: cartesianPowerAux T (@length T l) *)
unfold cartesianPower in IHl.
(* Goal: cartesianPowerAux T (@length T l) *)
simpl in IHl.
(* Goal: cartesianPowerAux T (@length T l) *)
rewrite minus_n_0 in IHl.
(* Goal: cartesianPowerAux T (@length T l) *)
exact IHl.
Defined.

Fixpoint circPermNCP {T:Type} {m:nat} (n : nat) (cp : cartesianPower T (S (S m))) :=
  match n with
  | 0 => cp
  | S p => circPermNCP p (consTailCP (tailCP cp) (headCP cp))
  end.

Lemma circPermNCP0 {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))),
  cp = circPermNCP 0 cp.
Proof.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
Qed.

Lemma circPermNCPOK {T:Type} {m:nat} :
  forall (n : nat) (cp : cartesianPower T (S (S m))),
  circPermNCP (S n) cp = circPermNCP n (consTailCP (tailCP cp) (headCP cp)).
Proof.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
unfold circPermNCP; reflexivity.
Qed.

Lemma nthCircPermNAny {T:Type} {m:nat} :
  forall (cp : cartesianPower T (S (S m))) (Default : T) id n,
  id + n <= S m -> nthCP (S id + n) cp Default = nthCP (S id) (circPermNCP n cp) Default.
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intros cp Default id n Hle; revert cp; induction n; intro cp.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
rewrite plus_n_0; simpl; reflexivity.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq T (@nthCP T (S (S m)) (Init.Nat.add (S id) (S n)) cp Default) (@nthCP T (S (S m)) (S id) (@circPermNCP T m n (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) Default) *)
assert (H : id + n <= S m) by (apply le_Sn_le; rewrite plus_n_Sm; assumption).
(* Goal: @eq T (@nthCP T (S (S m)) (Init.Nat.add (S id) (S n)) cp Default) (@nthCP T (S (S m)) (S id) (@circPermNCP T m n (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) Default) *)
assert (H' : id + n <= m) by (apply le_S_n; transitivity (id + S n); intuition).
(* Goal: @NoDup A (@cons A a l) *)
rewrite <- IHn; try assumption.
(* Goal: @eq T (@nthCP T (S (S m)) (Init.Nat.add (S id) (S n)) cp Default) (@nthCP T (S (S m)) (Init.Nat.add (S id) n) (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp)) Default) *)
rewrite <- plus_n_Sm.
(* Goal: @NoDup A (@cons A a l) *)
apply nthCircPerm2Eq; assumption.
Qed.

Lemma circPermNIdFirst {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) (Default : T),
  nthCP 1 cp Default = nthCP 1 (circPermNCP (S (S n)) cp) Default.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (_ : T), @eq (cartesianPower T (S (S n))) cp (@circPermNCP T n (S (S n)) cp) *)
intros cp Default.
(* Goal: @eq T (@nthCP T (S (S n)) (S O) cp Default) (@nthCP T (S (S n)) (S O) (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite nthCircPerm1Eq.
(* Goal: ge (S id) (S O) *)
assert (H : 0 + S n <= S n) by intuition.
(* Goal: @eq T (@nthCP T (S (S n)) (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) (@nthCP T (S (S n)) (S O) (@circPermNCP T n (S (S n)) cp) Default) *)
assert (H' := nthCircPermNAny (consTailCP (tailCP cp) (headCP cp)) Default 0 (S n) H); clear H.
(* Goal: @eq T (@nthCP T (S (S n)) (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp)) Default) (@nthCP T (S (S n)) (S O) (@circPermNCP T n (S (S n)) cp) Default) *)
assert (H : 1 + S n = S (S n)) by intuition; rewrite H in H'; clear H; rewrite H'.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) (@circPermNCP T (S (S n)) (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp))) *)
apply eq_sym.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma circPermNConsTlOK {T:Type} {m:nat} :
  forall (n : nat) (cp : cartesianPower T (S (S m))),
  consTailCP (tailCP (circPermNCP n cp)) (headCP (circPermNCP n cp)) = circPermNCP n (consTailCP (tailCP cp) (headCP cp)).
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intros n; induction n; intro cp.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) (@circPermNCP T (S (S n)) (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp))) *)
apply eq_sym.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq (cartesianPower T (S (S m))) (@circPermNCP T m n (@consTailCP T (S m) (@tailCP T m (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) (@headCP T (S m) (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))))) (@consTailCP T (S m) (@tailCP T m (@circPermNCP T m (S n) cp)) (@headCP T (S m) (@circPermNCP T m (S n) cp))) *)
rewrite <- IHn.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite <- circPermNCPOK.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma circPermPerm {T:Type} {m:nat} :
  forall (n : nat) (cp : cartesianPower T (S (S m))),
  circPermNCP (S (S (S n))) cp = circPermNCP 1 (circPermNCP (S (S n)) cp).
Proof.
(* Goal: forall (n : nat) (cp : cartesianPower T (S (S m))), @eq (cartesianPower T (S (S m))) (@circPermNCP T m (S (S (S n))) cp) (@circPermNCP T m (S O) (@circPermNCP T m (S (S n)) cp)) *)
intros n cp.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) (@circPermNCP T (S (S n)) (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp))) *)
apply eq_sym.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq (cartesianPower T (S (S m))) (@circPermNCP T m O (@consTailCP T (S m) (@tailCP T m (@circPermNCP T m (S (S n)) cp)) (@headCP T (S m) (@circPermNCP T m (S (S n)) cp)))) (@circPermNCP T m (S (S n)) (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) *)
rewrite <- circPermNCP0.
(* Goal: @eq (cartesianPower T (S (S m))) (@consTailCP T (S m) (@tailCP T m (@circPermNCP T m (S (S n)) cp)) (@headCP T (S m) (@circPermNCP T m (S (S n)) cp))) (@circPermNCP T m (S (S n)) (@consTailCP T (S m) (@tailCP T m cp) (@headCP T (S m) cp))) *)
apply circPermNConsTlOK.
Qed.

Lemma nthCP01 {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) Default,
  nthCP 0 cp Default = nthCP 1 cp Default.
Proof.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
unfold nthCP.
(* Goal: forall (cp : cartesianPower T (S n)) (Default : T), @eq T (@nth T (Init.Nat.sub O (S O)) (@CPToList T (S n) cp) Default) (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S n) cp) Default) *)
assert (H : 0 - 1 = 0) by (simpl; reflexivity); rewrite H; clear H.
(* Goal: forall (cp : cartesianPower T (S n)) (Default : T), @eq T (@nth T O (@CPToList T (S n) cp) Default) (@nth T (Init.Nat.sub (S O) (S O)) (@CPToList T (S n) cp) Default) *)
assert (H : 1 - 1 = 0) by (simpl; reflexivity); rewrite H; clear H.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma circPermNIdAux {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))) (Default : T),
  cp = circPermNCP (S (S n)) cp.
Proof.
(* Goal: forall (cp : cartesianPower T (S (S n))) (_ : T), @eq (cartesianPower T (S (S n))) cp (@circPermNCP T n (S (S n)) cp) *)
intros cp Default.
(* Goal: @eq (cartesianPower T (S (S n))) cp (@circPermNCP T n (S (S n)) cp) *)
apply nthEqOK with Default.
(* Goal: forall n0 : nat, @eq T (@nthCP T (S (S n)) n0 cp Default) (@nthCP T (S (S n)) n0 (@circPermNCP T n (S (S n)) cp) Default) *)
intro m.
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
assert (Hmn := le_lt_dec m (S (S n))).
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
elim Hmn; clear Hmn; intro Hmn.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
revert cp; induction m; intro cp.
(* Goal: @eq T (@nthCP T (S (S n)) O cp Default) (@nthCP T (S (S n)) O (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
do 2 (rewrite nthCP01).
(* Goal: @eq T (@nthCP T (S (S n)) (S O) cp Default) (@nthCP T (S (S n)) (S O) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) (S (S m)) cp Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
apply circPermNIdFirst.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
clear IHm.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
revert cp; induction m; intro cp.
(* Goal: @eq T (@nthCP T (S (S n)) (S O) cp Default) (@nthCP T (S (S n)) (S O) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) (S (S m)) cp Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
apply circPermNIdFirst.
(* Goal: @eq T (@nthCP T (S (S n)) (S (S m)) cp Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
assert (H : m <= n) by (do 2 (apply le_S_n); assumption).
(* Goal: @eq T (@nthCP T (S (S n)) (S (S m)) cp Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite nthCircPerm2Eq; try assumption; clear H.
(* Goal: ge (S id) (S O) *)
assert (H : S m <= S (S n)) by intuition.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite IHm; try assumption; clear H; clear IHm.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) (@consTailCP T (S n) (@tailCP T n cp) (@headCP T (S n) cp))) Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite <- circPermNCPOK.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S (S n))) cp) Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite circPermPerm.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S O) (@circPermNCP T n (S (S n)) cp)) Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
assert (H : m + 1 <= S n) by (rewrite plus_n_1; intuition).
(* Goal: @eq T (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S O) (@circPermNCP T n (S (S n)) cp)) Default) (@nthCP T (S (S n)) (S (S m)) (@circPermNCP T n (S (S n)) cp) Default) *)
(* Goal: @eq T (@nthCP T (S (S n)) m cp Default) (@nthCP T (S (S n)) m (@circPermNCP T n (S (S n)) cp) Default) *)
rewrite <- nthCircPermNAny; try assumption; clear H.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
rewrite plus_n_1; reflexivity.
(* Goal: Prop *)
induction m.
(* Goal: ge (S id) (S O) *)
assert (H := lt_n_0 (S (S n))); intuition.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
clear IHm.
(* Goal: @eq T (@nthCP T (S (S n)) (S m) cp Default) (@nthCP T (S (S n)) (S m) (@circPermNCP T n (S (S n)) cp) Default) *)
unfold nthCP.
(* Goal: @eq T (@nth T (Init.Nat.sub (S m) (S O)) (@CPToList T (S (S n)) cp) Default) (@nth T (Init.Nat.sub (S m) (S O)) (@CPToList T (S (S n)) (@circPermNCP T n (S (S n)) cp)) Default) *)
rewrite nth_overflow.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
rewrite nth_overflow; try reflexivity.
(* Goal: le (@length T (@CPToList T (S (S n)) cp)) (Init.Nat.sub (S m) (S O)) *)
rewrite <- lengthOfCPToList.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: le (S (S n)) (Init.Nat.sub m O) *)
rewrite minus_n_0.
(* Goal: le (S (S n)) m *)
apply gt_S_le.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
(* Goal: le (@length T (@CPToList T (S (S n)) cp)) (Init.Nat.sub (S m) (S O)) *)
rewrite <- lengthOfCPToList.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
simpl.
(* Goal: le (S (S n)) (Init.Nat.sub m O) *)
rewrite minus_n_0.
(* Goal: le (S (S n)) m *)
apply gt_S_le.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
Qed.

Lemma circPermNId {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S (S n))),
  cp = circPermNCP (S (S n)) cp.
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: @eq (cartesianPower T (S (S n))) cp (@circPermNCP T n (S (S n)) cp) *)
apply circPermNIdAux.
(* Goal: T *)
exact (headCP cp).
Qed.

Lemma circPermNConsOK {T:Type} {n:nat} :
  forall (cp : cartesianPower T (S n)) (t1 t2 : T),
  circPermNCP (S n) (consTailCP (consTailCP cp t1) t2) = consHeadCP t1 (consHeadCP t2 cp).
Proof.
(* Goal: forall (cp : cartesianPower T (S n)) (t1 t2 : T), @eq (cartesianPower T (S (S (S n)))) (@circPermNCP T (S n) (S n) (@consTailCP T (S (S n)) (@consTailCP T (S n) cp t1) t2)) (@consHeadCP T (S (S n)) t1 (@consHeadCP T (S n) t2 cp)) *)
induction n; intros cp t1 t2.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
clear IHn.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp)) *)
assert (H := circPermNId (consHeadCP t1 (consHeadCP t2 cp))); rewrite H; clear H.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) (@circPermNCP T (S (S n)) (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp))) *)
apply eq_sym.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S (S n))) (@consTailCP T (S (S (S n))) (@tailCP T (S (S n)) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp))) (@headCP T (S (S (S n))) (@consHeadCP T (S (S (S n))) t1 (@consHeadCP T (S (S n)) t2 cp))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) *)
assert (H : headCP (consHeadCP t1 (consHeadCP t2 cp)) = t1) by (simpl; reflexivity); rewrite H; clear H.
assert (H : tailCP (consHeadCP t1 (consHeadCP t2 cp)) = consHeadCP t2 cp)
(* Goal: @NoDup A l *)
  by (simpl; reflexivity); rewrite H; clear H.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: @eq (cartesianPower T (S (S (S (S n))))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@tailCP T (S (S n)) (@consTailCP T (S (S (S n))) (@consHeadCP T (S (S n)) t2 cp) t1)) (@headCP T (S (S (S n))) (@consTailCP T (S (S (S n))) (@consHeadCP T (S (S n)) t2 cp) t1)))) (@circPermNCP T (S (S n)) (S (S n)) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) cp t1) t2)) *)
assert (H : headCP (consTailCP (consHeadCP t2 cp) t1) = t2) by (simpl; reflexivity); rewrite H; clear H.
assert (H : tailCP (consTailCP (consHeadCP t2 cp) t1) = consTailCP cp t1)
(* Goal: @NoDup A l *)
  by (simpl; reflexivity); rewrite H; clear H.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma listInd {T : Type} : forall n (l l' : list T) Default,
  length l = (S n) ->
  length l' = (S n) ->
  hd Default l = hd Default l' ->
  tl l = tl l' ->
  l = l'.
Proof.
(* Goal: forall (n : nat) (l l' : list T) (Default : T) (_ : @eq nat (@length T l) (S n)) (_ : @eq nat (@length T l') (S n)) (_ : @eq T (@hd T Default l) (@hd T Default l')) (_ : @eq (list T) (@tl T l) (@tl T l')), @eq (list T) l l' *)
intros n l.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.
(* Goal: forall (l' : list T) (Default : T) (_ : @eq nat (@length T (@nil T)) (S n)) (_ : @eq nat (@length T l') (S n)) (_ : @eq T (@hd T Default (@nil T)) (@hd T Default l')) (_ : @eq (list T) (@tl T (@nil T)) (@tl T l')), @eq (list T) (@nil T) l' *)
(* Goal: forall (l' : list T) (Default : T) (_ : @eq nat (@length T (@cons T a l)) (S n)) (_ : @eq nat (@length T l') (S n)) (_ : @eq T (@hd T Default (@cons T a l)) (@hd T Default l')) (_ : @eq (list T) (@tl T (@cons T a l)) (@tl T l')), @eq (list T) (@cons T a l) l' *)
intros l' Default Hl.
(* Goal: forall (_ : @eq nat (@length T l') (S n)) (_ : @eq T (@hd T Default (@nil T)) (@hd T Default l')) (_ : @eq (list T) (@tl T (@nil T)) (@tl T l')), @eq (list T) (@nil T) l' *)
(* Goal: forall (l' : list T) (Default : T) (_ : @eq nat (@length T (@cons T a l)) (S n)) (_ : @eq nat (@length T l') (S n)) (_ : @eq T (@hd T Default (@cons T a l)) (@hd T Default l')) (_ : @eq (list T) (@tl T (@cons T a l)) (@tl T l')), @eq (list T) (@cons T a l) l' *)
simpl in Hl; discriminate.
(* Goal: forall (l' : list T) (Default : T) (_ : @eq nat (@length T (@cons T a l)) (S n)) (_ : @eq nat (@length T l') (S n)) (_ : @eq T (@hd T Default (@cons T a l)) (@hd T Default l')) (_ : @eq (list T) (@tl T (@cons T a l)) (@tl T l')), @eq (list T) (@cons T a l) l' *)
intros l' Default Hl Hl' Hhd Htl.
(* Goal: @Permutation.Permutation A (@cons A a l) l' *)
induction l'.
(* Goal: @eq (list T) (@cons T a l) (@nil T) *)
(* Goal: @eq (list T) (@cons T a l) (@cons T a0 l') *)
simpl in Hl'; discriminate.
(* Goal: @eq (list T) (@cons T a l) (@cons T a0 l') *)
simpl in Hhd.
(* Goal: @eq (list T) (@cons T a l) (@cons T a0 l') *)
simpl in Htl.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
subst.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Lemma CPLHd {T : Type} :
  forall (a : T) l Default,
  hd Default (CPToList (ListToCP (a :: l) Default)) = a.
Proof.
(* Goal: forall (a : T) (l : list T) (Default : T), @eq (list T) (@cons T a (@CPToList T (@length T l) (@ListToCP T l Default))) (@CPToList T (@length T (@cons T a l)) (@ListToCP T (@cons T a l) Default)) *)
intros a l Default.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
Qed.

Lemma ListToCPTl {T : Type} :
  forall (a a0 : T) l (Ha0l : (S (length l)) = length (a0  :: l)) Haa0l Default,
  tailCPbis (length (a :: a0 :: l)) (length (a :: l)) (ListToCP (a :: a0 :: l) Default) Haa0l Ha0l =
  ListToCP (a0 :: l) Default.
Proof.
(* Goal: forall (a a0 : T) (l : list T) (Ha0l : @eq nat (S (@length T l)) (@length T (@cons T a0 l))) (Haa0l : @eq nat (S (S (@length T l))) (@length T (@cons T a (@cons T a0 l)))) (Default : T), @eq (cartesianPower T (@length T (@cons T a l))) (@tailCPbis T (@length T l) (@length T (@cons T a (@cons T a0 l))) (@length T (@cons T a l)) (@ListToCP T (@cons T a (@cons T a0 l)) Default) Haa0l Ha0l) (@ListToCP T (@cons T a0 l) Default) *)
intros a a0 l Ha0l Haa0l Default.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
simpl in *.
(* Goal: @eq (cartesianPower T (@length T (@cons T a0 l))) (@tailCPbis T (@length T l) (@length T (@cons T a (@cons T a0 l))) (@length T (@cons T a l)) (@ListToCP T (@cons T a (@cons T a0 l)) Default) Haa0l Ha0l) (@tailCP T ((fix length (l : list T) : nat := match l with | nil => O | cons a l' => S (length l') end) l) (@ListToCP T (@cons T a (@cons T a0 l)) Default)) *)
unfold tailCPbis.
(* Goal: @eq (cartesianPower T (S (@length T l))) (@eq_rect nat (S (S (@length T l))) (fun m1 : nat => forall _ : cartesianPower T m1, cartesianPower T (S (@length T l))) (fun cp : cartesianPower T (S (S (@length T l))) => @eq_rect nat (S (@length T l)) (fun m2 : nat => cartesianPower T m2) (@tailCP T (@length T l) cp) (S (@length T l)) Ha0l) (S (S (@length T l))) Haa0l (@pair T (cartesianPowerAux T (@length T l)) a (@eq_rect nat (Init.Nat.sub (@length T l) O) (fun n : nat => cartesianPowerAux T n) (@list_rect T (fun l : list T => forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (fun _ : cartesianPower T O => a0) (fun (_ : T) (l : list T) (_ : forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (IHl : cartesianPower T (S (@length T l))) => @pair T (cartesianPowerAux T (@length T l)) a0 (@eq_rect nat (Init.Nat.sub (@length T l) O) (fun n : nat => cartesianPowerAux T n) IHl (@length T l) (minus_n_0 (@length T l)))) l (@ListToCP T l Default)) (@length T l) (minus_n_0 (@length T l))))) (@list_rect T (fun l : list T => forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (fun _ : cartesianPower T O => a0) (fun (_ : T) (l : list T) (_ : forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (IHl : cartesianPower T (S (@length T l))) => @pair T (cartesianPowerAux T (@length T l)) a0 (@eq_rect nat (Init.Nat.sub (@length T l) O) (fun n : nat => cartesianPowerAux T n) IHl (@length T l) (minus_n_0 (@length T l)))) l (@ListToCP T l Default)) *)
unfold tailCP.
(* Goal: @eq (cartesianPower T (S (@length T l))) (@eq_rect nat (S (S (@length T l))) (fun m1 : nat => forall _ : cartesianPower T m1, cartesianPower T (S (@length T l))) (fun cp : cartesianPower T (S (S (@length T l))) => @eq_rect nat (S (@length T l)) (fun m2 : nat => cartesianPower T m2) (nat_rect (fun n : nat => forall _ : cartesianPower T (S (S n)), cartesianPower T (S n)) (fun cp0 : cartesianPower T (S (S O)) => @snd T T cp0) (fun (n : nat) (_ : forall _ : cartesianPower T (S (S n)), cartesianPower T (S n)) (cp0 : cartesianPower T (S (S (S n)))) => @snd T (prod T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp0) (@length T l) cp) (S (@length T l)) Ha0l) (S (S (@length T l))) Haa0l (@pair T (cartesianPowerAux T (@length T l)) a (@eq_rect nat (Init.Nat.sub (@length T l) O) (fun n : nat => cartesianPowerAux T n) (@list_rect T (fun l : list T => forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (fun _ : cartesianPower T O => a0) (fun (_ : T) (l : list T) (_ : forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (IHl : cartesianPower T (S (@length T l))) => @pair T (cartesianPowerAux T (@length T l)) a0 (@eq_rect nat (Init.Nat.sub (@length T l) O) (fun n : nat => cartesianPowerAux T n) IHl (@length T l) (minus_n_0 (@length T l)))) l (@ListToCP T l Default)) (@length T l) (minus_n_0 (@length T l))))) (@list_rect T (fun l : list T => forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (fun _ : cartesianPower T O => a0) (fun (_ : T) (l : list T) (_ : forall _ : cartesianPower T (@length T l), cartesianPower T (S (@length T l))) (IHl : cartesianPower T (S (@length T l))) => @pair T (cartesianPowerAux T (@length T l)) a0 (@eq_rect nat (Init.Nat.sub (@length T l) O) (fun n : nat => cartesianPowerAux T n) IHl (@length T l) (minus_n_0 (@length T l)))) l (@ListToCP T l Default)) *)
repeat (elim_eq_rect; simpl).
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
induction l; simpl; reflexivity.
Qed.

Lemma CPToListTl1 {T : Type} :
  forall (a a0 : T) l (cp : cartesianPower T (length (a :: a0 :: l))), tl (CPToList cp) = CPToList (tailCP cp).
Proof.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
Qed.

Lemma CPToListTl2 {T : Type} {n : nat} :
  forall (cp : cartesianPower T (S (S n))), tl (CPToList cp) = CPToList (tailCP cp).
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (list T) (@tl T (@CPToList T (S (S (S n))) cp)) (@CPToList T (S (S n)) (@tailCP T (S n) cp)) *)
apply listInd with (S n) (fst cp).
(* Goal: @eq nat (@length T (@tl T (@CPToList T (S (S (S n))) cp))) (S (S n)) *)
(* Goal: @eq nat (@length T (@CPToList T (S (S n)) (@tailCP T (S n) cp))) (S (S n)) *)
(* Goal: @eq T (@hd T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) (@tl T (@CPToList T (S (S (S n))) cp))) (@hd T (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cp) (@CPToList T (S (S n)) (@tailCP T (S n) cp))) *)
(* Goal: @eq (list T) (@tl T (@tl T (@CPToList T (S (S (S n))) cp))) (@tl T (@CPToList T (S (S n)) (@tailCP T (S n) cp))) *)
apply eq_add_S.
(* Goal: @eq T t (@nth T id (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) Default) *)
assert (H := lengthOfCPToList cp); rewrite H.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq T t (@nth T id (@app T (@cons T (@headCP T (S n) cp) (@nil T)) (@CPToList T (S n) (@tailCP T n cp))) Default) *)
assert (H := lengthOfCPToList (tailCP cp)); rewrite H.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
Qed.

Lemma CPCPL {T : Type} :
  forall (a : T) l (cp1 : cartesianPower T (length (a :: l)))
  (cp2 : cartesianPower T (S(length l))),
  cp1 = cp2 -> CPToList cp1 = CPToList cp2.
Proof.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
intros; subst; reflexivity.
Qed.

Lemma CPLCP {T : Type} {n : nat} :
  forall (cp1 cp2 : cartesianPower T (S n)),
  CPToList cp1 = CPToList cp2 -> cp1 = cp2.
Proof.
(* Goal: forall (cp1 cp2 : cartesianPower T (S n)) (_ : @eq (list T) (@CPToList T (S n) cp1) (@CPToList T (S n) cp2)), @eq (cartesianPower T (S n)) cp1 cp2 *)
induction n; intros cp1 cp2 HCPL.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @eq (cartesianPower T (S O)) cp1 cp2 *)
(* Goal: @eq (cartesianPower T (S (S n))) cp1 cp2 *)
  injection HCPL.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
  auto.

(* Goal: @eq (cartesianPower T (S (S n))) cp1 cp2 *)
  do 2 (rewrite CPToListOK in HCPL).
(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
  apply CP_ind.

(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    injection HCPL; auto.

(* Goal: @eq (cartesianPower T (S n)) (@tailCP T n cp1) (@tailCP T n cp2) *)
    apply IHn.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    injection HCPL; auto.
Qed.

Lemma CPLRec {T : Type} :
  forall (a : T) l Default,
  (a :: (CPToList (ListToCP l Default))) = CPToList (ListToCP (a :: l) Default).
Proof.
(* Goal: forall (a : T) (l : list T) (Default : T), @eq (list T) (@cons T a (@CPToList T (@length T l) (@ListToCP T l Default))) (@CPToList T (@length T (@cons T a l)) (@ListToCP T (@cons T a l) Default)) *)
intros a l Default.
(* Goal: @eq (list T) (@cons T a (@CPToList T (@length T l) (@ListToCP T l Default))) (@CPToList T (@length T (@cons T a l)) (@ListToCP T (@cons T a l) Default)) *)
assert (HlAux := lengthOfCPToList (ListToCP l Default)).
assert (Hl : S (length l) = length (a :: CPToList (ListToCP l Default))) by (simpl; apply eq_S; assumption);
clear HlAux; apply eq_sym in Hl.
(* Goal: @eq (list T) (@cons T a (@CPToList T (@length T l) (@ListToCP T l Default))) (@CPToList T (@length T (@cons T a l)) (@ListToCP T (@cons T a l) Default)) *)
assert (Hal := lengthOfCPToList (ListToCP (a :: l) Default)); apply eq_sym in Hal.
(* Goal: @NoDup A (@cons A a l) *)
apply listInd with (length l) Default; try assumption.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
rewrite CPLHd; simpl; reflexivity.
assert (H : tl (a :: CPToList (ListToCP l Default)) = CPToList (ListToCP l Default)) by (simpl; reflexivity);
(* Goal: @NoDup A l *)
rewrite H; clear H.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (list T) (@CPToList T (@length T (@cons T a0 l)) (@ListToCP T (@cons T a0 l) Default)) (@tl T (@CPToList T (@length T (@cons T a (@cons T a0 l))) (@ListToCP T (@cons T a (@cons T a0 l)) Default))) *)
clear IHl.
(* Goal: @eq (list T) (@CPToList T (@length T (@cons T a0 l)) (@ListToCP T (@cons T a0 l) Default)) (@tl T (@CPToList T (@length T (@cons T a (@cons T a0 l))) (@ListToCP T (@cons T a (@cons T a0 l)) Default))) *)
assert (H := CPToListTl1 a a0 l (ListToCP (a :: a0 :: l) Default)); rewrite H; clear H.
assert (H := CPCPL a0 l (ListToCP (a0 :: l) Default) (tailCP (ListToCP (a :: a0 :: l) Default)));
(* Goal: @NoDup A l *)
apply H; clear H.
assert (Ha0l : (S (length l)) = length (a0  :: l)) by (simpl; reflexivity).
assert (Haa0l : (S (S (length l))) = length (a :: a0  :: l)) by (simpl; reflexivity).
(* Goal: @eq (cartesianPower T (@length T (@cons T a0 l))) (@ListToCP T (@cons T a0 l) Default) (@tailCP T ((fix length (l : list T) : nat := match l with | nil => O | cons a l' => S (length l') end) l) (@ListToCP T (@cons T a (@cons T a0 l)) Default)) *)
assert (H := ListToCPTl a a0 l Ha0l Haa0l Default); rewrite <- H; clear H.
(* Goal: @eq (cartesianPower T (@length T (@cons T a0 l))) (@tailCPbis T (@length T l) (@length T (@cons T a (@cons T a0 l))) (@length T (@cons T a l)) (@ListToCP T (@cons T a (@cons T a0 l)) Default) Haa0l Ha0l) (@tailCP T ((fix length (l : list T) : nat := match l with | nil => O | cons a l' => S (length l') end) l) (@ListToCP T (@cons T a (@cons T a0 l)) Default)) *)
unfold tailCPbis.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
repeat (elim_eq_rect; simpl); reflexivity.
Qed.

Lemma CPLOK {T : Type} : forall (l : list T) Default,
  CPToList (ListToCP l Default) = l.
Proof.
(* Goal: forall (l : list T) (Default : T), @eq (list T) (@CPToList T (@length T l) (@ListToCP T l Default)) l *)
intros l Default.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.
(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
simpl; reflexivity.
(* Goal: @eq (list T) (@CPToList T (@length T (@cons T a l)) (@ListToCP T (@cons T a l) Default)) (@cons T a l) *)
rewrite <- CPLRec.
(* Goal: @eq (list T) (@cons T a (@CPToList T (@length T l) (@ListToCP T l Default))) (@cons T a l) *)
rewrite IHl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
reflexivity.
Qed.

Definition fixLastCP {T:Type} {n:nat} (appPred : cartesianPower T (S (S n)) -> Prop) (t : T) : cartesianPower T (S n) -> Prop.
Proof.
(* Goal: forall _ : cartesianPower T (S n), Prop *)
intro cp.
(* Goal: Prop *)
apply appPred.
(* Goal: cartesianPower T (S (S n)) *)
exact (consTailCP cp t).
Defined.

Lemma fixLastCPOK {T:Type} {n:nat} :
  forall (appPred : cartesianPower T (S (S n)) -> Prop) (cp : cartesianPower T (S n)) (t : T),
  appPred (consTailCP  cp t) = (fixLastCP appPred t) cp.
Proof.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
intros appPred cp; unfold fixLastCP; reflexivity.
Qed.

Definition app {T:Type} {n:nat} (pred : arity T n) (cp : cartesianPower T n) : Prop.
Proof.
(* Goal: Prop *)
induction n; [apply pred|clear IHn].
(* Goal: Prop *)
induction n; [exact (pred cp)|exact (IHn (pred (headCP cp)) (tailCP cp))].
Defined.

Definition app_n_1 {T:Type} {n:nat} (pred : arity T (S n)) (cp : cartesianPower T n) (x : T) : Prop.
Proof.
(* Goal: Prop *)
induction n; [exact (pred x)|clear IHn].
(* Goal: Prop *)
induction n; [exact (pred cp x)|exact (IHn (pred (headCP cp)) (tailCP cp))].
Defined.

Lemma app_n_1_app {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x : T)
         (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))),
    app_n_1 pred cpp x -> allButLastCP cpt = cpp -> lastCP cpt = x ->
    app pred cpt.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: pred (@fst T T cpt) (@snd T T cpt) *)
(* Goal: @app T (S (S (S n))) pred cpt *)
  rewrite H0; rewrite H1.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  apply IHn with (tailCP cpp); clear IHn.

(* Goal: @app_n_1 T (S n) (pred (@headCP T (S (S n)) cpt)) (@tailCP T n cpp) x *)
(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    unfold app_n_1 in *.
(* Goal: nat_rect (fun n : nat => forall (_ : arity T n) (_ : cartesianPower T n), Prop) (fun (pred : arity T O) (_ : cartesianPower T O) => pred) (fun (n : nat) (_ : forall (_ : arity T n) (_ : cartesianPower T n), Prop) (pred : arity T (S n)) (cp : cartesianPower T (S n)) => nat_rect (fun n0 : nat => forall (_ : arity T (S n0)) (_ : cartesianPower T (S n0)), Prop) (fun (pred0 : arity T (S O)) (cp0 : cartesianPower T (S O)) => pred0 cp0) (fun (n0 : nat) (IHn0 : forall (_ : arity T (S n0)) (_ : cartesianPower T (S n0)), Prop) (pred0 : arity T (S (S n0))) (cp0 : cartesianPower T (S (S n0))) => IHn0 (pred0 (@headCP T (S n0) cp0)) (@tailCP T n0 cp0)) n pred cp) (S (S n)) (pred (@headCP T (S n) cpp)) (@tailCP T (S n) cpt) *)
(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    assert (H3 : (fst cpt) = fst (cpp)) by (rewrite <- H0; simpl; reflexivity).
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
    simpl in *.
(* Goal: nat_rect (fun n : nat => forall (_ : forall (_ : T) (_ : T), arity T n) (_ : cartesianPower T (S n)), Prop) (fun (pred : forall (_ : T) (_ : T), Prop) (cp : cartesianPower T (S O)) => pred cp x) (fun (n : nat) (IHn : forall (_ : forall (_ : T) (_ : T), arity T n) (_ : cartesianPower T (S n)), Prop) (pred : forall (_ : T) (_ : T) (_ : T), arity T n) (cp : cartesianPower T (S (S n))) => IHn (pred (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp)) (@tailCP T n cp)) n (pred (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    rewrite H3.
(* Goal: False *)
    apply H.

(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    rewrite <- H0.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
    induction n.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
      simpl; reflexivity.

(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
      apply CP_ind.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
        simpl; reflexivity.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
        simpl in *; reflexivity.

(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    rewrite <- H1.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
    induction n.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
      simpl; reflexivity.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
      simpl; reflexivity.
Qed.

Lemma app_app_n_1 {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))),
  app pred cpt -> allButLastCP cpt = cpp -> lastCP cpt = x ->
  app_n_1 pred cpp x.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
  rewrite <- H0; rewrite <- H1.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  apply IHn with (tailCP cpt); clear IHn.

(* Goal: @app T (S (S n)) (pred (@headCP T (S n) cpp)) (@tailCP T (S n) cpt) *)
(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    unfold app in *.
(* Goal: nat_rect (fun n : nat => forall (_ : arity T n) (_ : cartesianPower T n), Prop) (fun (pred : arity T O) (_ : cartesianPower T O) => pred) (fun (n : nat) (_ : forall (_ : arity T n) (_ : cartesianPower T n), Prop) (pred : arity T (S n)) (cp : cartesianPower T (S n)) => nat_rect (fun n0 : nat => forall (_ : arity T (S n0)) (_ : cartesianPower T (S n0)), Prop) (fun (pred0 : arity T (S O)) (cp0 : cartesianPower T (S O)) => pred0 cp0) (fun (n0 : nat) (IHn0 : forall (_ : arity T (S n0)) (_ : cartesianPower T (S n0)), Prop) (pred0 : arity T (S (S n0))) (cp0 : cartesianPower T (S (S n0))) => IHn0 (pred0 (@headCP T (S n0) cp0)) (@tailCP T n0 cp0)) n pred cp) (S (S n)) (pred (@headCP T (S n) cpp)) (@tailCP T (S n) cpt) *)
(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    assert (H3 : (fst cpt) = fst (cpp)) by (rewrite <- H0; simpl; reflexivity).
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
    simpl in *.
(* Goal: nat_rect (fun n : nat => forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (fun (pred : forall _ : T, Prop) (cp : cartesianPower T (S O)) => pred cp) (fun (n : nat) (IHn : forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (pred : forall (_ : T) (_ : T), arity T n) (cp : cartesianPower T (S (S n))) => IHn (pred (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp)) (@tailCP T n cp)) n (pred (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cpp) (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt))) (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt)) *)
(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    rewrite <- H3.
(* Goal: False *)
    apply H.

(* Goal: @eq (cartesianPower T (S n)) (@allButLastCP T n (@tailCP T (S n) cpt)) (@tailCP T n cpp) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    rewrite <- H0.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
    induction n.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
      simpl; reflexivity.

(* Goal: @eq (cartesianPower T (S (S n))) (@allButLastCP T (S n) (@tailCP T (S (S n)) cpt)) (@tailCP T (S n) (@allButLastCP T (S (S n)) cpt)) *)
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
      apply CP_ind.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
        simpl; reflexivity.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
        simpl in *; reflexivity.

(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
    rewrite <- H1.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
    induction n.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
      simpl; reflexivity.

(* Goal: @eq T (@lastCP T (S (S n)) (@tailCP T (S (S n)) cpt)) (@lastCP T (S (S (S n))) cpt) *)
      simpl; reflexivity.
Qed.

Lemma app_n_1_app_eq {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))),
  allButLastCP cpt = cpp -> lastCP cpt = x ->
  (app pred cpt <-> app_n_1 pred cpp x).
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.

(* Goal: forall _ : @app_1_n T (S n) pred x cpp, @app T (S (S n)) pred cpt *)
  intro H1.
(* Goal: @app_n_1 T (S n) pred cpp x *)
(* Goal: forall _ : @app_n_1 T (S n) pred cpp x, @app T (S (S n)) pred cpt *)
  apply (app_app_n_1 pred x cpp cpt H1 H H0).

(* Goal: forall _ : @app_1_n T (S n) pred x cpp, @app T (S (S n)) pred cpt *)
  intro H1.
(* Goal: @app T (S (S n)) pred cpt *)
  apply (app_n_1_app pred x cpp cpt H1 H H0).
Qed.

Definition app_1_n {T:Type} {n:nat} (pred : arity T (S n)) (x : T) (cp : cartesianPower T n) : Prop.
Proof.
(* Goal: Prop *)
induction n; [exact (pred x)|clear IHn].
(* Goal: Prop *)
induction n; [exact (pred x cp)|clear IHn].
(* Goal: Prop *)
assert (newPred : arity T (S n)) by (exact (pred x (headCP cp))).
(* Goal: Prop *)
exact (app newPred (tailCP cp)).
Defined.

Lemma app_1_n_app {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))),
  app_1_n pred x cpp -> headCP cpt = x -> tailCP cpt = cpp ->
  app pred cpt.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: pred (@fst T T cpt) (@snd T T cpt) *)
(* Goal: @app T (S (S (S n))) pred cpt *)
  rewrite H0; rewrite H1.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  clear IHn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: pred (@fst T T cpt) (@snd T T cpt) *)
(* Goal: @app T (S (S (S n))) pred cpt *)
  rewrite H0; rewrite H1.
(* Goal: False *)
  apply H.
Qed.

Lemma app_app_1_n {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))),
  app pred cpt -> headCP cpt = x -> tailCP cpt = cpp ->
  app_1_n pred x cpp.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
  rewrite <- H0; rewrite <- H1.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  clear IHn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @eq T (@lastCP T (S n) (@tailCP T (S n) cpt)) x *)
  rewrite <- H0; rewrite <- H1.
(* Goal: False *)
  apply H.
Qed.

Lemma app_1_n_app_eq {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S n))),
  headCP cpt = x -> tailCP cpt = cpp ->
  (app pred cpt <-> app_1_n pred x cpp).
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.

(* Goal: forall _ : @app_1_n T (S n) pred x cpp, @app T (S (S n)) pred cpt *)
  intro H1.
(* Goal: @app_1_n T (S n) pred x cpp *)
(* Goal: forall _ : @app_1_n T (S n) pred x cpp, @app T (S (S n)) pred cpt *)
  apply (app_app_1_n pred x cpp cpt H1 H H0).

(* Goal: forall _ : @app_1_n T (S n) pred x cpp, @app T (S (S n)) pred cpt *)
  intro H1.
(* Goal: @app T (S (S n)) pred cpt *)
  apply (app_1_n_app pred x cpp cpt H1 H H0).
Qed.

Definition app_2_n {T:Type} {n:nat} (pred : arity T (S (S n))) (x1 x2 : T) (cp : cartesianPower T n) : Prop.
Proof. exact (app (pred x1 x2) cp). Defined.

Lemma app_2_n_app {T:Type} {n:nat} :
  forall (pred : arity T (S (S (S n)))) (x1 x2 : T)
  (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))),
  app_2_n pred x1 x2 cpp -> headCP cpt = x1 -> headCP (tailCP cpt) = x2 -> tailCP (tailCP cpt) = cpp ->
  app pred cpt.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: nat_rect (fun n : nat => forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (fun (pred : forall _ : T, Prop) (cp : cartesianPower T (S O)) => pred cp) (fun (n : nat) (IHn : forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (pred : forall (_ : T) (_ : T), arity T n) (cp : cartesianPower T (S (S n))) => IHn (pred (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp)) (@tailCP T n cp)) n (pred (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt) (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt))) (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt)) *)
  rewrite H0; rewrite H1; rewrite H2.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  clear IHn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: nat_rect (fun n : nat => forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (fun (pred : forall _ : T, Prop) (cp : cartesianPower T (S O)) => pred cp) (fun (n : nat) (IHn : forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (pred : forall (_ : T) (_ : T), arity T n) (cp : cartesianPower T (S (S n))) => IHn (pred (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp)) (@tailCP T n cp)) n (pred (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt) (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt))) (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt)) *)
  rewrite H0; rewrite H1; rewrite H2.
(* Goal: False *)
  apply H.
Qed.

Lemma app_2_n_app_default {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x1 x2 : T)
  (cpp Default : cartesianPower T n) (cpt : cartesianPower T (S (S n))),
  app_2_n pred x1 x2 cpp -> headCP cpt = x1 ->
  headCP (tailCP cpt) = x2 ->
  tailDefaultCP (tailCP cpt) Default = cpp ->
  app pred cpt.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: pred (@fst T T cpt) (@snd T T cpt) *)
(* Goal: @app T (S (S (S n))) pred cpt *)
  rewrite H0; rewrite H1.
(* Goal: False *)
  apply H.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: nat_rect (fun n : nat => forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (fun (pred : forall _ : T, Prop) (cp : cartesianPower T (S O)) => pred cp) (fun (n : nat) (IHn : forall (_ : forall _ : T, arity T n) (_ : cartesianPower T (S n)), Prop) (pred : forall (_ : T) (_ : T), arity T n) (cp : cartesianPower T (S (S n))) => IHn (pred (@fst T ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) cp)) (@tailCP T n cp)) n (pred (@fst T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt) (@fst T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n) (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt))) (@tailCP T n (@snd T (prod T ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) T n)) cpt)) *)
  rewrite H0; rewrite H1; rewrite H2.
(* Goal: False *)
  apply H.
Qed.

Lemma app_app_2_n {T:Type} {n:nat} :
  forall (pred : arity T (S (S (S n)))) (x1 x2 : T)
  (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))),
  app pred cpt -> headCP cpt = x1 -> headCP (tailCP cpt) = x2 -> tailCP (tailCP cpt) = cpp ->
  app_2_n pred x1 x2 cpp.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  rewrite <- H0; rewrite <- H1; rewrite <- H2.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  clear IHn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  rewrite <- H0; rewrite <- H1; rewrite <- H2.
(* Goal: False *)
  apply H.
Qed.

Lemma app_app_2_n_default {T:Type} {n:nat} :
  forall (pred : arity T (S (S n))) (x1 x2 : T)
  (cpp Default : cartesianPower T n) (cpt : cartesianPower T (S (S n))),
  app pred cpt -> headCP cpt = x1 -> headCP (tailCP cpt) = x2 -> tailDefaultCP (tailCP cpt) Default = cpp ->
  app_2_n pred x1 x2 cpp.
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.

(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  rewrite <- H0; rewrite <- H1; rewrite <- H2.
(* Goal: False *)
  apply H.

(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  clear IHn.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
  rewrite <- H0; rewrite <- H1; rewrite <- H2.
(* Goal: False *)
  apply H.
Qed.

Lemma app_2_n_app_eq {T:Type} {n:nat} :
  forall (pred : arity T (S (S (S n)))) (x1 x2 : T)
  (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))),
  headCP cpt = x1 -> headCP (tailCP cpt) = x2 -> tailCP (tailCP cpt) = cpp ->
  (app pred cpt <-> app_2_n pred x1 x2 cpp).
Proof.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
intros.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
split.

(* Goal: forall _ : @app_2_n T (S n) pred x1 x2 cpp, @app T (S (S (S n))) pred cpt *)
  intro H2.
(* Goal: @app_2_n T (S n) pred x1 x2 cpp *)
(* Goal: forall _ : @app_2_n T (S n) pred x1 x2 cpp, @app T (S (S (S n))) pred cpt *)
  apply (app_app_2_n pred x1 x2 cpp cpt H2 H H0 H1).

(* Goal: forall _ : @app_2_n T (S n) pred x1 x2 cpp, @app T (S (S (S n))) pred cpt *)
  intro H2.
(* Goal: @app T (S (S (S n))) pred cpt *)
  apply (app_2_n_app pred x1 x2 cpp cpt H2 H H0 H1).
Qed.

Lemma PermOKAux {T : Type} {m : nat} :
  forall (appPred : (cartesianPower T (S (S m))) -> Prop) n,
  (forall (A : T) (X : cartesianPower T (S m)), appPred (consHeadCP A X) -> appPred (consTailCP X A)) ->
  (forall (X : cartesianPower T (S (S m))),
          appPred X -> appPred (circPermNCP n X)).
Proof.
(* Goal: forall (appPred : forall _ : cartesianPower T (S (S m)), Prop) (n : nat) (_ : forall (A : T) (X : cartesianPower T (S m)) (_ : appPred (@consHeadCP T (S m) A X)), appPred (@consTailCP T (S m) X A)) (X : cartesianPower T (S (S m))) (_ : appPred X), appPred (@circPermNCP T m n X) *)
intros appPred n HPerm.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
induction n.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
simpl; auto.
(* Goal: forall (X : cartesianPower T (S (S m))) (_ : appPred X), appPred (@circPermNCP T m (S n) X) *)
intros X HappPred.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
assert (H : appPred (circPermNCP n X)) by (apply IHn; assumption); clear IHn; clear HappPred.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite consHeadCPOK in H.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
apply HPerm in H.
(* Goal: appPred (@circPermNCP T m (S n) X) *)
rewrite circPermNCPOK.
(* Goal: appPred (@circPermNCP T m n (@consTailCP T (S m) (@tailCP T m X) (@headCP T (S m) X))) *)
rewrite <- circPermNConsTlOK.
(* Goal: @NoDup A (@cons A a l) *)
assumption.
Qed.

Lemma PermOK {T : Type} {n : nat} :
  forall (cp1 cp2 : cartesianPower T (S (S n))) (appPred : (cartesianPower T (S (S n))) -> Prop),
  (forall (A : T) (X : cartesianPower T (S n)),
    appPred (consHeadCP A X) -> appPred (consTailCP X A)) ->
  (forall (A B : T) (X : cartesianPower T n),
    appPred (consHeadCP A (consHeadCP B X)) -> appPred (consHeadCP B (consHeadCP A X))) ->
  appPred cp1 ->
  Permutation.Permutation (CPToList cp1) (CPToList cp2) ->
  appPred cp2.
Proof.
(* Goal: forall (cp1 cp2 : cartesianPower T (S (S n))) (appPred : forall _ : cartesianPower T (S (S n)), Prop) (_ : forall (A : T) (X : cartesianPower T (S n)) (_ : appPred (@consHeadCP T (S n) A X)), appPred (@consTailCP T (S n) X A)) (_ : forall (A B : T) (X : cartesianPower T n) (_ : appPred (@consHeadCP T (S n) A (@consHeadCP T n B X))), appPred (@consHeadCP T (S n) B (@consHeadCP T n A X))) (_ : appPred cp1) (_ : @Permutation.Permutation T (@CPToList T (S (S n)) cp1) (@CPToList T (S (S n)) cp2)), appPred cp2 *)
induction n; intros cp1 cp2 appPred pred_perm_1 pred_perm_2 Hpred HPerm.

(* Goal: appPred cp2 *)
(* Goal: appPred cp2 *)
  assert (Hcp1 := CPPair cp1); rewrite Hcp1 in *; clear Hcp1.
(* Goal: appPred cp2 *)
(* Goal: appPred cp2 *)
  assert (Hcp2 := CPPair cp2); rewrite Hcp2 in *; clear Hcp2.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  simpl in *.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  apply Permutation.Permutation_length_2 in HPerm.
(* Goal: appPred (@pair T T (@fst T T cp2) (@snd T T cp2)) *)
(* Goal: appPred cp2 *)
  elim HPerm; clear HPerm; intro HPerm; destruct HPerm as [HEq1 HEq2]; rewrite <- HEq1; rewrite <- HEq2.

(* Goal: @NoDup A (@cons A a l) *)
    assumption.

(* Goal: @NoDup A (@cons A a l) *)
    apply pred_perm_1; assumption.

(* Goal: appPred cp2 *)
  rewrite consTailCPOK.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
  assert (H' := lastCPIn cp2).
  assert (H : InCP (lastCP cp2) cp1)
    by (unfold InCP;apply Permutation.Permutation_in with (CPToList cp2);
        try apply Permutation.Permutation_sym; assumption); clear H'.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
  assert (H' := InNth cp1 (lastCP cp2) (headCP cp2) H); clear H.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
  destruct H' as [id [Hge [Hle Hnth]]].
  assert (H : exists cp, appPred cp /\ Permutation.Permutation (CPToList cp2) (CPToList cp) /\
                                       lastCP cp = lastCP cp2).

(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
    induction id; try (unfold ge in Hge; assert (H := Le.le_Sn_0 0); contradiction); clear IHid.
(* Goal: forall (pred : arity T (S (S (S n)))) (x1 x2 : T) (cpp : cartesianPower T (S n)) (cpt : cartesianPower T (S (S (S n)))) (_ : @eq T (@headCP T (S (S n)) cpt) x1) (_ : @eq T (@headCP T (S n) (@tailCP T (S n) cpt)) x2) (_ : @eq (cartesianPower T (S n)) (@tailCP T n (@tailCP T (S n) cpt)) cpp), iff (@app T (S (S (S n))) pred cpt) (@app_2_n T (S n) pred x1 x2 cpp) *)
    revert Hnth; revert HPerm; revert Hpred; revert cp1; induction id; intros.

(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      exists (consTailCP (tailCP cp1) (headCP cp1)).
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
      split.

(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consHeadCP T (S (S (S (S n)))) E (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D))) A) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        apply pred_perm_1.
(* Goal: appPred (@consHeadCP T (S (S n)) (@headCP T (S (S n)) cp1) (@tailCP T (S n) cp1)) *)
(* Goal: and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) (@consTailCP T (S (S n)) (@tailCP T (S n) cp1) (@headCP T (S (S n)) cp1)))) (@eq T (@lastCP T (S (S n)) (@consTailCP T (S (S n)) (@tailCP T (S n) cp1) (@headCP T (S (S n)) cp1))) (@lastCP T (S (S n)) cp2)) *)
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
        rewrite <- consHeadCPOK.
(* Goal: @NoDup A (@cons A a l) *)
        assumption.

(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
        split.

(* Goal: @Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) (@consTailCP T (S (S n)) (@tailCP T (S n) cp1) (@headCP T (S (S n)) cp1))) *)
(* Goal: @eq T (@lastCP T (S (S n)) (@consTailCP T (S (S n)) (@tailCP T (S n) cp1) (@headCP T (S (S n)) cp1))) (@lastCP T (S (S n)) cp2) *)
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
          apply Permutation.perm_trans with (CPToList cp1); try (apply consTailPerm).
(* Goal: @NoDup A (@cons A a l) *)
          apply Permutation.Permutation_sym; assumption.

(* Goal: @eq T (@lastCP T (S (S n)) (@consTailCP T (S (S n)) (@tailCP T (S n) cp1) (@headCP T (S (S n)) cp1))) (@lastCP T (S (S n)) cp2) *)
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
          apply nthCircPerm1 in Hnth.
(* Goal: @eq T (@lastCP T (S (S n)) (@consTailCP T (S (S n)) (@tailCP T (S n) cp1) (@headCP T (S (S n)) cp1))) (@lastCP T (S (S n)) cp2) *)
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
          rewrite Hnth.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
          assert (H := nthLast (consTailCP (tailCP cp1) (headCP cp1)) (headCP cp2)); rewrite H; reflexivity.

(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      assert (H := Hle).
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      do 2 (apply Le.le_S_n in H).
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      apply nthCircPerm2 in Hnth; try assumption; clear H.
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      apply Le.le_Sn_le in Hle.
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      assert (H : S id >= 1) by intuition; clear Hge; rename H into Hge.
      assert (H : appPred (consTailCP (tailCP cp1) (headCP cp1)))
        by (apply pred_perm_1; rewrite <- consHeadCPOK; assumption) ; clear Hpred; rename H into Hpred.
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      assert (H := consTailPerm cp1); apply Permutation.Permutation_sym in H.
      assert (H' : Permutation.Permutation (CPToList (consTailCP (tailCP cp1) (headCP cp1))) (CPToList cp2))
        by (apply Permutation.perm_trans with (CPToList cp1); assumption); clear HPerm; rename H' into HPerm.
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      assert (H' := IHid Hge Hle (consTailCP (tailCP cp1) (headCP cp1)) Hpred HPerm Hnth).
(* Goal: @ex (cartesianPower T (S (S (S n)))) (fun cp : cartesianPower T (S (S (S n))) => and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2)))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      destruct H' as [cp [Hpredcp [HPermcp Hlastcp]]]; exists cp.
(* Goal: and (appPred cp) (and (@Permutation.Permutation T (@CPToList T (S (S (S n))) cp2) (@CPToList T (S (S (S n))) cp)) (@eq T (@lastCP T (S (S n)) cp) (@lastCP T (S (S n)) cp2))) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
      do 2 (split; try assumption).

(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
  clear Hnth; clear Hle; clear Hge; clear id; clear HPerm; clear Hpred; clear cp1.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp2)) *)
  destruct H as [cp [Hpred [HPerm Hlast]]]; rewrite <- Hlast.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  assert (H := consTailCPOK cp); rewrite H in HPerm; clear H.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  assert (H := consTailCPOK cp2); rewrite H in HPerm; clear H.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  do 2 (rewrite consTailOK in HPerm).
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  rewrite Hlast in HPerm.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  apply Permutation.Permutation_app_inv_r in HPerm.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  assert (ablcp := allButLastCP cp).
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  assert (ablcp2 := allButLastCP cp2).
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  assert (pred_perm_3 := PermOKAux appPred (S n) pred_perm_1).
  assert (HPerm1 : (forall (A : T) (X : cartesianPower T (S n)),
                   (fixLastCP appPred (lastCP cp)) (consHeadCP A X) ->
                   (fixLastCP appPred (lastCP cp)) (consTailCP X A))).

(* Goal: forall (A : T) (X : cartesianPower T (S n)) (_ : @fixLastCP T (S n) appPred (@lastCP T (S (S n)) cp) (@consHeadCP T (S n) A X)), @fixLastCP T (S n) appPred (@lastCP T (S (S n)) cp) (@consTailCP T (S n) X A) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
    unfold fixLastCP; intros A X HappPred.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
    induction n.

(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
      simpl in HappPred.
(* Goal: appPred (@consTailCP T (S (S O)) (@consTailCP T (S O) X A) (@lastCP T (S (S O)) cp)) *)
(* Goal: appPred (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) X A) (@lastCP T (S (S (S n))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
      apply pred_perm_2.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
      simpl.
(* Goal: @NoDup A (@cons A a l) *)
      assumption.

(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
      clear IHn0.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
      induction n.

(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
        simpl.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        simpl in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        simpl in pred_perm_1.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        simpl in pred_perm_2.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        apply pred_perm_2 in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        apply pred_perm_2 in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        apply pred_perm_3 in HappPred; simpl in HappPred.
(* Goal: @NoDup A (@cons A a l) *)
        assumption.

(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        clear IHn0.
(* Goal: appPred (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) X A) (@lastCP T (S (S (S (S n)))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
        induction n.

(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
          simpl.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          simpl in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          simpl in pred_perm_1.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          simpl in pred_perm_2.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_2 in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_2 in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_2 in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: appPred (@pair T (prod T (prod T (prod T T))) (@fst T (prod T T) X) (@pair T (prod T (prod T T)) (@fst T T (@snd T (prod T T) X)) (@pair T (prod T T) (@snd T T (@snd T (prod T T) X)) (@pair (cartesianPower T (S O)) T A (@snd T T (@snd T (prod T T) (@snd T (prod T (prod T T)) (@snd T (prod T (prod T (prod T T))) cp)))))))) *)
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1 in HappPred; simpl in HappPred.
(* Goal: @NoDup A (@cons A a l) *)
          assumption.

(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          clear IHn0.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) X A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          assert (H := consHeadCPOK X); rewrite H in *; clear H.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) (@headCP T (S (S (S n))) X) (@tailCP T (S (S n)) X)) A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          assert (H := consTailCPOK (tailCP X)); rewrite H in *; clear H.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) (@headCP T (S (S (S n))) X) (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) (@lastCP T (S (S n)) (@tailCP T (S (S n)) X)))) A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          set (B := headCP X) in *.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) (@lastCP T (S (S n)) (@tailCP T (S (S n)) X)))) A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          set (CP := allButLastCP (allButLastCP (tailCP X))) in *.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) (@lastCP T (S (S n)) (@tailCP T (S (S n)) X)))) A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          set (C := tailCP (allButLastCP (tailCP X))) in *.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) (@lastCP T (S (S n)) (@tailCP T (S (S n)) X)))) A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          set (D := lastCP (tailCP X)) in *.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) (@lastCP T (S (S (S (S (S n))))) cp)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          set (E := lastCP cp) in *.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_3 in HappPred; rewrite consTlHdHdTl in HappPred; rewrite circPermNConsOK in HappPred.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1 in HappPred; do 2 (rewrite <- consHdTlTlHd in HappPred).
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_2 in HappPred.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D)) A) E) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1; rewrite <- consHdTlTlHd; rewrite <- circPermNConsOK.
(* Goal: appPred (@circPermNCP T (S (S (S (S n)))) (S (S (S (S n)))) (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D) A) E) B)) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_3.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consTailCP T (S (S (S (S n)))) (@consTailCP T (S (S (S n))) (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D) A) E) B) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          do 2 (apply pred_perm_1; rewrite consHdTlTlHd); rewrite consHdTlTlHd.
(* Goal: appPred (@consTailCP T (S (S (S (S (S n))))) (@consHeadCP T (S (S (S (S n)))) E (@consHeadCP T (S (S (S n))) B (@consTailCP T (S (S n)) (@allButLastCP T (S n) (@tailCP T (S (S n)) X)) D))) A) *)
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
          apply pred_perm_1.
(* Goal: @NoDup A (@cons A a l) *)
          assumption.
  assert (HPerm2 : (forall (A B : T) (X : cartesianPower T n),
                   (fixLastCP appPred (lastCP cp)) (consHeadCP A (consHeadCP B X)) ->
                   (fixLastCP appPred (lastCP cp)) (consHeadCP B (consHeadCP A X))))
    by (unfold fixLastCP; intros A B X HappPred; rewrite <- consTlHdHdTl;
        apply pred_perm_2; rewrite consTlHdHdTl; assumption).
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  apply Permutation.Permutation_sym in HPerm.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp2) (@lastCP T (S (S n)) cp)) *)
  assert (H := IHn (allButLastCP cp) (allButLastCP cp2) (fixLastCP appPred (lastCP cp)) HPerm1 HPerm2).
(* Goal: @NoDup A (@cons A a l) *)
  apply H; try assumption.
(* Goal: @fixLastCP T (S n) appPred (@lastCP T (S (S n)) cp) (@allButLastCP T (S n) cp) *)
  rewrite <- fixLastCPOK.
(* Goal: appPred (@consTailCP T (S (S n)) (@allButLastCP T (S n) cp) (@lastCP T (S (S n)) cp)) *)
  rewrite <- consTailCPOK.
(* Goal: @NoDup A (@cons A a l) *)
  assumption.
Qed.

Lemma lengthNilOK {A : Type} : forall (l : list A),
  length l = 0 -> l = nil.
Proof.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
intros l Hlength; induction l.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
  reflexivity.

(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
  simpl in Hlength.
(* Goal: @Permutation.Permutation A (@cons A a l) (@nil A) *)
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a0 l') *)
  discriminate.
Qed.

Lemma NoDupOK {A : Type} : forall (l l' : list A),
  incl l l' ->
  length l = length l' ->
  NoDup l ->
  Permutation.Permutation l l'.
Proof.
(* Goal: forall (l l' : list A) (_ : @incl A l l') (_ : @eq nat (@length A l) (@length A l')) (_ : @NoDup A l), @Permutation.Permutation A l l' *)
intro l; induction l; intros l' Hincl Hlength HNoDup.

(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
  simpl in Hlength.
(* Goal: @Permutation.Permutation A (@nil A) l' *)
(* Goal: @Permutation.Permutation A (@cons A a l) l' *)
  apply eq_sym in Hlength.
(* Goal: @Permutation.Permutation A (@nil A) l' *)
(* Goal: @Permutation.Permutation A (@cons A a l) l' *)
  apply lengthNilOK in Hlength.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
  subst.
(* Goal: @Permutation.Permutation A (@nil A) (@nil A) *)
(* Goal: @Permutation.Permutation A (@cons A a l) l' *)
  apply Permutation.perm_nil.

(* Goal: @Permutation.Permutation A (@cons A a l) l' *)
  induction l'.

(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
    simpl in Hlength.
(* Goal: @Permutation.Permutation A (@cons A a l) (@nil A) *)
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a0 l') *)
    discriminate.

(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a0 l') *)
    clear IHl'.
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a0 l') *)
    rename a0 into a'.
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    assert (HIn := in_eq a l).
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    assert (H := Hincl).
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    unfold incl in H.
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    apply H in HIn.
(* Goal: @NoDup A l *)
    clear H.
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    apply in_split in HIn.
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    destruct HIn as [l1 [l2 Hl']].
(* Goal: @Permutation.Permutation A (@cons A a l) (@cons A a' l') *)
    rewrite Hl' in *.
(* Goal: @Permutation.Permutation A (@cons A a l) (@Datatypes.app A l1 (@cons A a l2)) *)
    apply Permutation.Permutation_cons_app.
(* Goal: @Permutation.Permutation A l (@Datatypes.app A l1 l2) *)
    apply IHl.

(* Goal: @incl A l (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      unfold incl.
(* Goal: forall (a : A) (_ : @In A a l), @In A a (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      intros e HIn.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      unfold incl in Hincl.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      assert (H := Hincl e).
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      clear Hincl.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      assert (HIn' := in_cons a e l HIn).
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      apply H in HIn'.
(* Goal: @NoDup A l *)
      clear H.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      apply in_app_or in HIn'.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      elim HIn'; clear HIn'; intro HIn'.

(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
        apply in_or_app.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
        auto.

(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
        apply in_inv in HIn'.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
        elim HIn'; clear HIn'; intro HIn'.

(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
          subst.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
          assert (H := NoDup_remove_2 nil l e).
(* Goal: @NoDup A l *)
          simpl in H.
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
          apply H in HNoDup.
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@nil A) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
          contradiction.

(* Goal: @In A e (@Datatypes.app A l1 l2) *)
(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
          apply in_or_app.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
          auto.

(* Goal: @eq nat (@length A l) (@length A (@Datatypes.app A l1 l2)) *)
(* Goal: @NoDup A l *)
      rewrite app_length.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
      rewrite app_length in Hlength.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
      simpl in Hlength.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
      rewrite <- plus_n_Sm in Hlength.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l1) (@length A l2)) *)
(* Goal: @NoDup A l *)
      apply eq_add_S in Hlength.
(* Goal: @NoDup A (@cons A a l) *)
      assumption.

(* Goal: @NoDup A l *)
      assert (H := NoDup_remove_1 nil l a).
(* Goal: @NoDup A l *)
      simpl in H.
(* Goal: False *)
      apply H.
(* Goal: @NoDup A (@cons A a l) *)
      assumption.
Qed.

Lemma NoDup_dec {A : Type} : forall (l : list A),
  (forall x y : A, {x = y} + {x <> y}) ->
  NoDup l \/ ~ NoDup l.
Proof.
(* Goal: forall (l : list A) (_ : forall x y : A, sumbool (@eq A x y) (not (@eq A x y))) (_ : not (@NoDup A l)), @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
intros l HDec.
(* Goal: or (@NoDup A l) (not (@NoDup A l)) *)
induction l.

(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
  left.
(* Goal: @NoDup A (@nil A) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
  apply NoDup_nil.

(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
  elim IHl; clear IHl; intro H.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    assert (HIn := in_dec HDec a l).
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    elim HIn; clear HIn; intro HIn.

(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
      right.
(* Goal: @NoDup A l *)
      clear H.
(* Goal: not (@NoDup A (@cons A a l)) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
      intro H.
(* Goal: False *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
      assert (H' := NoDup_remove_2 nil l a).
(* Goal: False *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
      simpl in H'.
(* Goal: False *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
      apply H' in H.
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@nil A) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
      contradiction.

(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
      left.
(* Goal: @NoDup A (@cons A a l) *)
      apply NoDup_cons; assumption.

(* Goal: or (@NoDup A (@cons A a l)) (not (@NoDup A (@cons A a l))) *)
    right.
(* Goal: not (@NoDup A (@cons A a l)) *)
    intro H'.
(* Goal: False *)
    apply H.
(* Goal: @NoDup A l *)
    clear H.
(* Goal: @NoDup A l *)
    assert (H := NoDup_remove_1 nil l a).
(* Goal: @NoDup A l *)
    simpl in H.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    auto.
Qed.

Lemma NotNoDupDup {A : Type} : forall (l : list A),
  (forall x y : A, {x = y} + {x <> y}) ->
  ~ NoDup l->
  exists e l1 l2, l = l1 ++ e :: l2 /\ In e (l1 ++ l2).
Proof.
(* Goal: forall (l : list A) (_ : forall x y : A, sumbool (@eq A x y) (not (@eq A x y))) (_ : not (@NoDup A l)), @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
intros l HDec.
(* Goal: forall _ : not (@NoDup A l), @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) l (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
induction l; intro HDup.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@nil A) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
  assert (H := NoDup_nil A).
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@nil A) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
  contradiction.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
  assert (HIn := in_dec HDec a l).
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
  elim HIn; clear HIn; intro HIn.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    exists a; exists nil; exists l.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
    simpl.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a l)) (@In A a l) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    auto.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    assert (HDup' := NoDup_dec l HDec).
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
    elim HDup'; clear HDup'; intro HDup'.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
      exfalso.
(* Goal: False *)
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
      apply HDup.
(* Goal: @NoDup A (@cons A a l) *)
      apply NoDup_cons; assumption.

(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
      apply IHl in HDup'.
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
      clear HDec; clear HDup; clear HIn.
(* Goal: @eq (list T) (@CPToList T (@length T (@cons T a0 l)) (@ListToCP T (@cons T a0 l) Default)) (@tl T (@CPToList T (@length T (@cons T a (@cons T a0 l))) (@ListToCP T (@cons T a (@cons T a0 l)) Default))) *)
      destruct HDup' as [e [l1 [l2 [HEq HIn]]]]; clear IHl.
(* Goal: @ex A (fun e : A => @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq (list A) (@cons A a l) (@Datatypes.app A l1 (@cons A e l2))) (@In A e (@Datatypes.app A l1 l2))))) *)
      exists e; exists (a :: l1); exists l2.
(* Goal: and (@eq (list A) (@cons A a l) (@Datatypes.app A (@cons A a l1) (@cons A e l2))) (@In A e (@Datatypes.app A (@cons A a l1) l2)) *)
      simpl.
(* Goal: and (@eq (list A) (@cons A a l) (@cons A a (@Datatypes.app A l1 (@cons A e l2)))) (or (@eq A a e) (@In A e (@Datatypes.app A l1 l2))) *)
      split.

(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
        rewrite HEq; reflexivity.

(* Goal: @NoDup A (@cons A a l) *)
        right; assumption.
Qed.

Definition pred_conj_aux {T:Type} {n:nat} (pred : arity T (S n)) (m : nat) (cp : cartesianPower T (S m)) (cpwd : cartesianPower T n) : Prop.
Proof.
(* Goal: Prop *)
induction m.
(* Goal: Prop *)
(* Goal: Prop *)
exact (app_1_n pred cp cpwd).
(* Goal: Prop *)
exact ((app_1_n pred (headCP cp) cpwd) /\ IHm (tailCP cp)).
Defined.

Lemma pcaHdTl {T:Type} {n:nat} : forall (pred : arity T (S n)) m cp cpwd,
  pred_conj_aux pred (S m) cp cpwd = (app_1_n pred (headCP cp) cpwd /\ pred_conj_aux pred m (tailCP cp) cpwd).
Proof.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
unfold pred_conj_aux; unfold nat_rect; reflexivity.
Qed.

Definition pred_conj {T:Type} {n:nat} (pred : arity T (S n)) (cp : cartesianPower T (S n)) (cpwd : cartesianPower T n) : Prop.
Proof.
(* Goal: Prop *)
exact (pred_conj_aux pred n cp cpwd).
Defined.
