Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
cmm':
(Atom
)
(Atom
).
i:Atom.
e:Exp. nat_evolves_assig(cmm';i;e)
Applied Tactic:
Unfold `nat_evolves_assig` 0 THEN Auto
Generated subgoals:
None
cmm':
(Atom 
) (Atom ). i:Atom. e:Exp. nat_evolves_assig(cmm';i;e) 
cmm': (Atom ) (Atom ). i:Atom. e:Exp. nat_evolves_assig(cmm';i;e)