English
If R is a relation, then Pairwise R (cons hd tl) holds whenever Pairwise R tl and hd relates to every element of tl.
Русский
Если R — отношение, то Pairwise R (cons hd tl) выполняется, если Pairwise R tl и hd относится к каждому элементу tl.
LaTeX
$$$\text{Pairwise } R\ (cons\ hd\ tl) \iff (\forall x \in tl,\ R\ hd\ x) \land \text{Pairwise } R\ tl$$$
Lean4
theorem cons {R : α → α → Prop} {hd : α} {tl : Seq α} (h_hd : ∀ x ∈ tl, R hd x) (h_tl : Pairwise R tl) :
Pairwise R (cons hd tl) := by
simp only [Pairwise] at *
intro i j h_ij x hx y hy
cases j with
| zero => simp at h_ij
| succ k =>
simp only [get?_cons_succ] at hy
cases i with
| zero =>
simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
exact hx ▸ all_get h_hd hy
| succ n => exact h_tl n k (by omega) x hx y hy
