English
A decomposition principle for HolorIndex: to prove a property for a cons-index, it suffices to check it at the head and recursively at the tail.
Русский
Принцип разложения индекса HolorIndex: чтобы доказать свойство для индекса вида i :: is, достаточно проверить его для головы и рекурсивно для хвоста.
LaTeX
$$$\forall p : HolorIndex\,(d::ds)\to Prop,\forall t, \big(\forall i\,is,\forall h, t=(i::is)\Rightarrow p⟨i::is, h⟩\big) \Rightarrow p t$$$
Lean4
theorem holor_index_cons_decomp (p : HolorIndex (d :: ds) → Prop) :
∀ t : HolorIndex (d :: ds), (∀ i is, ∀ h : t.1 = i :: is, p ⟨i :: is, by rw [← h]; exact t.2⟩) → p t
| ⟨[], hforall₂⟩, _ => absurd (forall₂_nil_left_iff.1 hforall₂) (cons_ne_nil d ds)
| ⟨i :: is, _⟩, hp => hp i is rfl
