proposition: Lemma nth_ext : forall l l' d d', length l = length l' -> (forall n, n < length l -> nth n l d = nth n l' d') -> l = l'.
proof: Proof. intro l; induction l as [|a l IHl]; intros l' d d' Hlen Hnth; destruct l' as [| b l']. - reflexivity. - inversion Hlen. - inversion Hlen. - change a with (nth 0 (a :: l) d). change b with (nth 0 (b :: l') d'). rewrite Hnth; f_equal. + apply IHl with d d'; [ now inversion Hlen | ]. intros n Hlen'; apply (Hnth (S n)). now apply (Nat.succ_lt_mono n (length l)). + simpl; apply Nat.lt_0_succ. Qed.
imports: PeanoNat