proposition: Lemma consTailPerm {T:Type} {n:nat} : forall (cp : cartesianPower T (S (S n))), Permutation.Permutation (CPToList cp) (CPToList (consTailCP (tailCP cp) (headCP cp))).
proof: Proof. intro cp. rewrite CPLHdTlOK. rewrite consTailOK. apply Permutation.Permutation_app_comm. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality