English
For any C : Finmap β → Finmap β → Finmap β → Prop, if C holds for all triples of Finmaps arising from ALists, then C holds for any triple (s1, s2, s3).
Русский
Для любого C : Finmap β → Finmap β → Finmap β → Prop, если C верно для всех троек Finmap, полученных из AList, то C верно и для любых s1, s2, s3.
LaTeX
$$$$ \forall {\alpha} {\beta} {C} (s_1 s_2 s_3 : Finmap β), (\forall a_1 a_2 a_3 : AList β, C a_1.toFinmap a_2.toFinmap a_3.toFinmap) \rightarrow C s_1 s_2 s_3 $$$$
Lean4
@[elab_as_elim]
theorem induction_on₃ {C : Finmap β → Finmap β → Finmap β → Prop} (s₁ s₂ s₃ : Finmap β)
(H : ∀ a₁ a₂ a₃ : AList β, C ⟦a₁⟧ ⟦a₂⟧ ⟦a₃⟧) : C s₁ s₂ s₃ :=
induction_on₂ s₁ s₂ fun l₁ l₂ => induction_on s₃ fun l₃ => H l₁ l₂ l₃
