Elif, U. Simply Typed Lambda Calculus with de Bruijn indices in Lean4 [Computer software]