proposition: Lemma nth_error_eq: forall A (L1 L2 : list A), (forall i, nth_error L1 i = nth_error L2 i) -> L1 = L2.
proof: Proof. induction L1. destruct L2; auto; intros. specialize (H 0%nat); discriminate. destruct L2. intro. specialize (H 0%nat); discriminate. intros. f_equal. specialize (H 0%nat). inversion H. trivial. apply IHL1. intro. specialize (H (S i)). apply H. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset