English
Define a motive on triples of vectors by case-analysis on v1, v2, v3. Nil nil nil is the base, and cons extends each head with tails, producing C (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs).
Русский
Определяем мотив для трёх векторов через разбор случаев по v1, v2, v3: базовый случай nil nil nil и операция cons, добавляющая головы к векторам-хвостам.
LaTeX
$$$\\text{casesOn₃}\\{motive\\} (v_1 : Vector α n) (v_2 : Vector β n) (v_3 : Vector γ n) (nil) (cons) : motive v_1 v_2 v_3$$$
Lean4
/-- Define `motive v₁ v₂ v₃` by case-analysis on `v₁ : Vector α n`, `v₂ : Vector β n`, and
`v₃ : Vector γ n`. -/
def casesOn₃ {motive : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort*} (v₁ : Vector α m) (v₂ : Vector β m)
(v₃ : Vector γ m) (nil : motive nil nil nil)
(cons :
∀ {n},
(x : α) →
(y : β) →
(z : γ) →
(xs : Vector α n) → (ys : Vector β n) → (zs : Vector γ n) → motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)) :
motive v₁ v₂ v₃ :=
inductionOn₃ (C := motive) v₁ v₂ v₃ nil @fun _ x y z xs ys zs _ => cons x y z xs ys zs
