An arithmetical proof of the strong normalization for the λ-calculus with recursive equations on types - René David; Karim Nour (2009)