proposition: Lemma CPToListTl1 {T : Type} : forall (a a0 : T) l (cp : cartesianPower T (length (a :: a0 :: l))), tl (CPToList cp) = CPToList (tailCP cp).
proof: Proof. simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality