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