Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

ev:( (Atom ) (Atom )) . cmm': (Atom ) (Atom ). b1:exp. c3,c4:. nat_evolves_if(ev;cmm';b1;c3;c4)

Applied Tactic: Unfold `nat_evolves_if` 0 THEN Auto
Generated subgoals:

None