proposition: Lemma lastCPIn {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)), InCP (lastCP cp) cp.
proof: Proof. unfold InCP. intro cp; induction n. simpl; intuition. simpl. assert (H := IHn (tailCP cp)). intuition. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality