proposition: Lemma CPLCP {T : Type} {n : nat} : forall (cp1 cp2 : cartesianPower T (S n)), CPToList cp1 = CPToList cp2 -> cp1 = cp2.
proof: Proof. induction n; intros cp1 cp2 HCPL. simpl in *. injection HCPL. auto. do 2 (rewrite CPToListOK in HCPL). apply CP_ind. injection HCPL; auto. apply IHn. injection HCPL; auto. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality