Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

v:Atom. e:Exp. m:Atom . [v := e](m) a.if a=v then [e] else (m a)

Applied Tactic: Unfold `evolves` 0 THEN UnivCD THENM With 1 (D 0) THENM RecCaseSplit `nth` THEN Auto
Generated subgoals:

1. <SKIP, a.if a=v then [e] else (m a)>[0] = <SKIP, a.if a=v then [e] else (m a)>