[Hol-info] Help for newbie

[Georg W. <geo...@gm...>]

I've a newbie question. How do prove the following subgoal (i.e., which tactic
should I use)?

(nextstate st press_accelerate).doors = closed
    ------------------------------------
      0.  ~(st.train = stopped) ==> (st.doors = closed)
      1.  ~((nextstate st press_accelerate).train = stopped)
     : goalstack

Thank you for your help,
Georg