proposition: Lemma lengthOfCPToList {T:Type} {n:nat} : forall (cp : cartesianPower T n), n = length (CPToList cp).
proof: Proof. intros. induction n. simpl. reflexivity. clear IHn. induction n. simpl. reflexivity. apply eq_S. apply IHn. Defined.
imports: Arith NArith List Sorting Coq.Program.Equality