Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

m:Atom . [SKIP](m) m

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

1. <SKIP, m>[0] = <SKIP, m>