English
If a property H maps Q a b to R a b for all a,b, then given Forall₂ Q l1 l2 and Forall₂ R l1 l2, one obtains Forall₂ S l1 l2 (a recursion pattern).
Русский
Если свойство H переводит Q a b в R a b для всех пар, то имея Forall₂ Q l1 l2 и Forall₂ R l1 l2, получаем Forall₂ S l1 l2 (рекурсивная схема).
LaTeX
$$$$ \\text{Given } h:\\forall a,b, Q a b \\to R a b,\\text{ then } Forall₂ Q l_1 l_2 \\to Forall₂ R l_1 l_2 \\to Forall₂ S l_1 l_2. $$$$
Lean4
theorem mp {Q : α → β → Prop} (h : ∀ a b, Q a b → R a b → S a b) :
∀ {l₁ l₂}, Forall₂ Q l₁ l₂ → Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂
| [], [], Forall₂.nil, Forall₂.nil => Forall₂.nil
| a :: _, b :: _, Forall₂.cons hr hrs, Forall₂.cons hq hqs => Forall₂.cons (h a b hr hq) (Forall₂.mp h hrs hqs)
