proposition: Lemma consTailOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) t, CPToList (consTailCP cp t) = CPToList cp ++ t :: nil.
proof: Proof. induction n; intros cp t. simpl; reflexivity. rewrite CPToListOK. assert (H : headCP (consTailCP cp t) = headCP cp) by (simpl; reflexivity); rewrite H; clear H. assert (H : tailCP (consTailCP cp t) = (consTailCP (tailCP cp) t)) by (simpl; reflexivity); rewrite H; clear H. rewrite IHn. simpl; reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality