# Lemmas for `list_find` in combination with `app` and `insert`.

This MR proposes an alternative to the lemmas for `list_find`

by @msammler in #131 (closed) (but that he removed later).

All lemmas are stated using a bi-implication, and they are strong enough to prove @msammler's original lemmas:

```
Lemma list_find_insert_Some_ne1 l i i' x x':
list_find P l = Some (i', x') → ¬ P x → i ≠ i' →
list_find P (<[i:=x]> l) = Some (i', x').
Proof.
rewrite list_find_insert_Some, !list_find_Some.
destruct (decide (i < i')); naive_solver eauto with lia.
Qed.
Lemma list_find_insert_Some_ne_change2 l i i' x x':
list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x' → i < i' →
list_find P l = Some (i, x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.
Lemma list_find_insert_Some_ne_same2 l i i' x x' x'':
list_find P (<[i:=x]>l) = Some (i', x') →
¬ P x → l !! i = Some x'' → (i < i' → ¬ P x'') →
list_find P l = Some (i', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver. Qed.
Lemma list_find_insert_Some_ne2 l i i' x x' x'':
list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x'' → (x'' = x' ∨ ¬ P x'') →
∃ i'', list_find P l = Some (i'', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.
```

I very much dislike the statement of `list_find_insert_Some`

, but I cannot come up with anything better that is true.