Prove in Agda the preservation and normalization properties for the language of Typed Arithmetic Expressions