proposition: Lemma consTailCPTlD {T:Type} {n:nat} : forall (cp : cartesianPower T n) t, tailDefaultCP (consHeadCP t cp) cp = cp.
proof: Proof. intros cp t; induction n; try (simpl; reflexivity). induction n; simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality