while_break_true.v

Theorem while_break_true : forall b c st st',
      (WHILE b DO c END) / st \\ SContinue / st' ->
      beval st' b = true ->
      exists st'', c / st'' \\ SBreak / st'.
  Proof.
    intros. remember (WHILE b DO c END) as Hloop.
    induction H; try (inversion HeqHloop); subst.
    congruence. apply IHceval2. auto. auto.
    apply IHceval. 

  b : bexp
  c : com
  st, st' : state
  H0 : beval st' b = true
  H1 : c / st \\ SBreak / st'
  IHceval : c = (WHILE b DO c END) ->
            beval st' b = true -> exists st'' : state, c / st'' \\ SBreak / st'
  H : beval st b = true
  HeqHloop : (WHILE b DO c END) = (WHILE b DO c END)
  ============================
  c = (WHILE b DO c END)

subgoal 2 (ID 626) is:
 beval st' b = true

Rather than applying IHceval, you can just do exists st.