Properties of List.enum

theorem List.forall_mem_zipIdx {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop} : (∀ (x : α × ℕ), x ∈ l.zipIdx n → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], n + i)

theorem List.forall_mem_zipIdx' {α : Type u_1} {l : List α} {p : α × ℕ → Prop} : (∀ (x : α × ℕ), x ∈ l.zipIdx → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], i)

Variant of forall_mem_zipIdx with the zipIdx argument specialized to 0.

theorem List.exists_mem_zipIdx {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop} : (∃ (x : α × ℕ), x ∈ l.zipIdx n ∧ p x) ↔ ∃ (i : ℕ), ∃ (x : i < l.length), p (l[i], n + i)

theorem List.exists_mem_zipIdx' {α : Type u_1} {l : List α} {p : α × ℕ → Prop} : (∃ (x : α × ℕ), x ∈ l.zipIdx ∧ p x) ↔ ∃ (i : ℕ), ∃ (x : i < l.length), p (l[i], i)

Variant of exists_mem_zipIdx with the zipIdx argument specialized to 0.