English
Define C on triples of vectors by induction on n, with nil nil nil as base and cons to extend each of the three vectors. Then C u v w holds for any vectors u, v, w of the same length.
Русский
Определяем C на тройке векторов через индукцию по длине, базовый случай nil nil nil и шаг cons, добавляющий по одному элементу к каждому из трёх векторов. Тогда C u v w выполняется для любых равной длины векторов.
LaTeX
$$$ C\\; u\\; v\\; w \\;\\text{ при условии: } nil\\ nil\\ nil\\; и\\; cons : ∀ {n} {a b c} {x : Vector α n} {y} {z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z) \\Rightarrow C\\, u\\, v\\, w $$$
Lean4
/-- Define `motive v₁ v₂` by case-analysis on `v₁ : Vector α n` and `v₂ : Vector β n`. -/
def casesOn₂ {motive : ∀ {n}, Vector α n → Vector β n → Sort*} (v₁ : Vector α m) (v₂ : Vector β m)
(nil : motive nil nil)
(cons : ∀ {n}, (x : α) → (y : β) → (xs : Vector α n) → (ys : Vector β n) → motive (x ::ᵥ xs) (y ::ᵥ ys)) :
motive v₁ v₂ :=
inductionOn₂ (C := motive) v₁ v₂ nil @fun _ x y xs ys _ => cons x y xs ys
