proposition: Lemma list_eq_same_length l1 l2 n : length l2 = n → length l1 = n → (∀ i x y, i < n → l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2.
proof: Proof. intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx. - destruct (lookup_lt_is_Some_2 l1 i) as [y Hy]. { rewrite Hlen; eauto using lookup_lt_Some. } rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some. - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None. Qed.
imports: stdpp(options)