Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

b:exp. c1,c2:. m,m':Atom . [b](m) [IF b THEN c1 ELSE c2 ](m) m' [c2](m) m'

Applied Tactic: Unfold `evolves` 0 THEN UnivCD THENM D (-1) THENA Auto
Generated subgoals:

1. n:. <c2, m>[n] = <SKIP, m'>