English
If a list l is Forall₂-related to l1 ++ l2, then the initial segment take(length l1) l is Forall₂-related to l1.
Русский
Если список l связанRelation Forall₂ с l1 ++ l2, то начальный префикс длины l1 связан Forall₂ с l1.
LaTeX
$$$ \forall l:\mathrm{List}\,\alpha\,\forall l_1:\mathrm{List}\,\beta\forall l_2:\mathrm{List}\,\beta,\ \mathrm{Forall₂}\ R\ l\ (\mathrm{l_1}\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!$$$
Lean4
theorem forall₂_take_append (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) :
Forall₂ R (List.take (length l₁) l) l₁ :=
by
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) := forall₂_take (length l₁) h
rwa [take_left] at h'
