Example of typed lambda term with recomputed argument What is an example of a typed lambda term $\lambda x.\phi : A \to B$ and a term $a : A$ such that, when $\beta$-reducing the term $(\lambda x.\phi)(a)$, the argument $a$ must be repeated/recomputed several times?
In the simply typed $\lambda$-calculus with pairs, a simple example is

$$(\lambda x :T. (x,x))a$$ 

where $a$ is a term of type $T$.