Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization