Finitary Corecursion for the Infinitary Lambda Calculus

Application: Corecursive Definitions on Rational λ-Trees

subs : νL.α × V × νL.α → νL.α