proposition: 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: Proof. intros; subst; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality