proposition: 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: Proof. intros. induction n; simpl in *; apply injective_projections; assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality