Towards the average-case analysis of substitution resolution in λ-calculus.