English
If a is accessible under r whenever f a is accessible under s, then a is accessible under r.
Русский
Если из доступности $f(a)$ следует доступность $a$, то $a$ доступен по отношению $r$.
LaTeX
$$$\forall f\ a,\ Acc\ s (f\ a) \Rightarrow Acc\ r\ a$$$
Lean4
protected theorem acc [RelHomClass F r s] (f : F) (a : α) : Acc s (f a) → Acc r a :=
by
generalize h : f a = b
intro ac
induction ac generalizing a with
| intro _ H IH => ?_
subst h
exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩