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