proposition: Lemma nthFirst {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) (t Default : T), t = nthCP 1 cp Default -> t = headCP cp.
proof: Proof. induction n; intros cp t Default Hnth. unfold nthCP in Hnth. simpl in Hnth. assumption. unfold nthCP in Hnth. simpl in Hnth. assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality