  The goal of this note is to supply proofs of two theorems stated [AGKRRV],
which deal with the Local Term map for the Frobenius endomorphism of Artin
stacks of finite type over F_q. Namely, we show that the "true local terms" of
the Frobenius endomorphism coincide with the "naive local terms" and that the
"naive local terms" commute with !-pushforwards. The latter result is a
categorical version of the classical Grothendieck-Lefschetz trace formula.
