```I managed to prove it using the prelude lemma "lub_nat" to get
at the largest natural less than j where the train is safe, and
measure-induct+ so that the induction works from i+1 to i.  I'm
making no claims that it is the best proof, but here it is:

(""
(grind :if-match nil)
(lemma "lub_nat")
(inst -1 "{i | i < j!1 AND train!1(i) = safe}" "j!1")
(("1"
(grind :if-match nil)
(inst 1 "n!1")
(assert)
(case "FORALL (k: upto(j!1)): n!1 < k IMPLIES train!1(k) = approaching")
(("1" (skosimp) (inst -1 "m!1") (assert))
("2"
(hide 2)
(measure-induct+ "j!1 - k" ("k"))
(inst -1 "x!1 + 1")
(("1" (assert) (inst -8 "x!1") (assert) (inst -5 "x!1") (assert))
("2" (assert))))))
("2" (grind))))

Note that using measure-induct+ directly on the original
formula leads to an unprovable TCC; this is due to the
heuristics used by measure-induct+ to create the induction
formula.  The case step just provides an alternative equivalent
form that works.

Sam

> I can not prove the following lemma.
>
> This THEORY is a part of railload crossing.
>
> ===========
>
> test: THEORY
> BEGIN
>
> train_state: TYPE = { safe, approaching, crossing}
> Train: TYPE = [ nat -> train_state ]
> train: VAR Train
> i, j, k, m: VAR nat
>
>
> test_lemma: LEMMA
> (FORALL i: train(i+1) = approaching IMPLIES
>   train(i) = approaching OR train(i) = safe) AND
> train(0) = safe AND
> train(j) = approaching
>
> IMPLIES
>
>   (EXISTS k:
>     k < j AND train(k) = safe AND
>     (FORALL m:
>       k < m AND m <= j IMPLIES
>         train(m) = approaching ))
>
> END test
>
> ===========
>
>