Description: Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was extracted from a former cbvabv version. (Contributed by Wolf Lammen, 16-Mar-2025)