proposition: Lemma consHdTlTlHd {T:Type} {n:nat} : forall (F L : T) (X : cartesianPower T n), consHeadCP F (consTailCP X L) = consTailCP (consHeadCP F X) L.
proof: Proof. induction n. intros F L X. unfold consHeadCP; unfold consTailCP; simpl; reflexivity. clear IHn. induction n. intros F L X. unfold consHeadCP; unfold consTailCP; simpl; reflexivity. intros F L X. apply CP_ind. simpl; reflexivity. assert (H := consHeadCPOK X); rewrite H; clear H. rewrite consHeadCPTl. rewrite consTailCPTl. rewrite consHeadCPTl. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality