feat: `List.forall_get_iff_forall_mem `

[Qiu233]

theorem forall_mem_iff_forall_index [DecidableEq α] {p : α → Prop} {l : List α} :
  (∀ x ∈ l, p x) ↔ (∀ i : Fin (l.length), p (l.get i))

is trivial but sometimes useful.

[Qiu233]

awaiting-review

[digama0]

I usually obtain the headline theorem using simp [List.mem_iff_get]. The other stuff is more API surface that should probably be considered in its own PR.

[Qiu233]

I usually obtain the headline theorem using simp [List.mem_iff_get]. The other stuff is more API surface that should probably be considered in its own PR.

Sorry I didn't find this theorem. Now other stuff has been removed.