\inferrule[\rulestyle{s-sym-nat-arr-update}]
  { \sestartconf{\mem}{e_{1}}{\cstr}\ssebstep\sefinalconf{v_{1}}{\cstr'}\and \sestartconf{\mem}{e_{2}}{\cstr'}\ssebstep\sefinalconf{v_{2}}{\cstr''}\\
    \sestartconf{\mem}{\metavar}{\cstr''}\ssebstep\sefinalconf{f}{\cstr'''}\and f:\mathbb{N}\mapsto\mathbb{N}\and \\
    f'=\lambda i.
    % \begin{cases*}
    %     v_2,& \text{if } i=v_{1}\\
    %     f(i),              & \text{otherwise}
    % \end{cases*}
      \and
      v_{1}>0
    }
    {\sscconf{\mem}{\ass{\metavar[e_{1}]}{e_{2}}}{\cstr}\sscmstep\sscconf{\mem[\metavar\mapsto f']}{\skipp}{\cstr'''}}