proposition: Lemma CPToListOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))), CPToList cp = cons (headCP cp) (CPToList (tailCP cp)).
proof: Proof. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality