T. M. . Galoyan, “Analysis of Bounds for Lengths of Reductions in Typed λ-calculus”, MPCS, vol. 29, pp. 5–15, Dec. 2021.