Nuprl - Pf add_action

1. St: Type
2. l: St*
3. f: StSt
4. s: St
5. u: St
6. v: St*
7. mem_f(St;s;v) mem_f(St;s;(+f)(v))

u = s mem_f(St;s;v) u = s f(u) = s mem_f(St;s;(+f)(v))

By: GenExRepD

Generated subgoals:

1 8. u = s
u = s f(u) = s mem_f(St;s;(+f)(v))

2 8. mem_f(St;s;v)
u = s f(u) = s mem_f(St;s;(+f)(v))

About:

1	8. `u = s` `u = s f(u) = s mem_f(St;s;(+f)(v))`
2	8. `mem_f(St;s;v)` `u = s f(u) = s mem_f(St;s;(+f)(v))`