proposition: Lemma consTailCPAbl {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) t, allButLastCP (consTailCP cp t) = cp.
proof: Proof. intros cp t; induction n; try (simpl; reflexivity). apply CP_ind. simpl; reflexivity. rewrite <- IHn. rewrite <- consTailCPTl. rewrite allButLastCPTl. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality