proposition: Lemma listInd {T : Type} : forall n (l l' : list T) Default, length l = (S n) -> length l' = (S n) -> hd Default l = hd Default l' -> tl l = tl l' -> l = l'.
proof: Proof. intros n l. induction l. intros l' Default Hl. simpl in Hl; discriminate. intros l' Default Hl Hl' Hhd Htl. induction l'. simpl in Hl'; discriminate. simpl in Hhd. simpl in Htl. subst. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality