proposition: Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
proof: Proof. revert l2. induction l1 as [|x l1 IH]; intros [|y l2] H. - done. - discriminate (H 0). - discriminate (H 0). - f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)). Qed.
imports: stdpp(options)