proposition: Lemma nthEqOK {T:Type} {m:nat} : forall (cp1 cp2 : cartesianPower T (S m)) (Default : T), (forall n, nthCP n cp1 Default = nthCP n cp2 Default) -> cp1 = cp2.
proof: Proof. induction m; intros cp1 cp2 Default Hnth. assert (H := Hnth 1). unfold nthCP in H. simpl in H. assumption. apply CP_ind. assert (H := Hnth 1). unfold nthCP in H. simpl in H. assumption. apply IHm with Default. intro n; induction n. assert (H := Hnth 2). unfold nthCP. unfold nthCP in H. do 2 (rewrite CPLHdTlOK in H). simpl; assumption. do 2 (rewrite nthCPTlOK). apply Hnth. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality