proposition: Lemma nth_error_ext l l': (forall n, nth_error l n = nth_error l' n) -> l = l'.
proof: Proof. revert l'. induction l as [|a l IHl]; intros l' Hnth; destruct l'. - reflexivity. - discriminate (Hnth 0). - discriminate (Hnth 0). - injection (Hnth 0) as ->. f_equal. apply IHl. intro n. exact (Hnth (S n)). Qed.
imports: PeanoNat