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