Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

ev:( (Atom ) (Atom )) . cmm': (Atom ) (Atom ). b2:exp. c5:. nat_evolves_while(ev;cmm';b2;c5)

Applied Tactic: Unfold `nat_evolves_while` 0 THEN UnivCD THENA Auto
Generated subgoals:

1. if [b2](cmm'.2.1) then m1:Atom . ev <c5, cmm'.2.1, m1> ev <WHILE b2 DO c5 OD, m1, cmm'.2.2> else cmm'.2.1 = cmm'.2.2 fi