English
If the relation r is RightUnique, then a certain lifting of Forall₂ r along Perm is possible: given Forall₂ r a b and Forall₂ r c d with a ~ c, one can deduce b ~ d.
Русский
Если отношение r имеет свойство правой уникальности, то при подстановке через Perm возможно поднять связь Forall₂ r: если a ~ c и Forall₂ r a b, Forall₂ r c d, то b ~ d.
LaTeX
$$$\\text{If }\\mathrm{RightUnique}(r)\\text{, then }\\forall a,b,c,d\\; (\\mathrm{Forall}_2(r)\,a\,b \\land \\mathrm{Forall}_2(r)\,c\,d \\land a \\sim c) \\Rightarrow b \\sim d$$$
Lean4
theorem rel_perm_imp (hr : RightUnique r) : (Forall₂ r ⇒ Forall₂ r ⇒ (· → ·)) Perm Perm := fun a b h₁ c d h₂ h =>
have : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d := ⟨a, h₁, c, h, h₂⟩
have : ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d := by
rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← Relation.comp_assoc] at this
let ⟨b', ⟨_, hbc, hcb⟩, hbd⟩ := this
have : b' = b := right_unique_forall₂' hr hcb hbc
this ▸ hbd
