Grind rules for `Automata.NA.addHist`

[chenson2018]

There are some places in #188 where this definition requires the use of simp to reduce the underlying NA. This isn't a big issue, but I unsuccessfully spent a while trying to determine what would be some nice grind lemmas. Opening this so we can revisit later.

[ctchou]

I played around with this issue a bit. I wonder if it is the same issue as #174. We have the notion of an infinite run of an NA:
def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) := ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))
Here the na is an NA.addHist construction. There are two problems, both of which are related to the second conjunct:

(1) When (na.addHist ...).Run appears among the hypotheses, grind is incapable of figuring out that:
∀ n, (na.addHist ...).Tr (ss n) (xs n) (ss (n + 1))
But if you add the above fact manually to the hypotheses, grind works.

(2) When (na.addHist ...).Run appears as the goal, grind is incapable of "seeing throughthe definition ofaddHistdespite of thegrind =annotation onaddHist. But once addHistis unfolded by any means,grind` works.