proposition: Lemma list_lookup_other l i x : length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y.
proof: Proof. intros. destruct i, l as [|x0 [|x1 l]]; simplify_eq/=. - by exists 1, x1. - by exists 0, x0. Qed.
imports: stdpp(options)