At: add action mem 3 2 1 1
1. St: Type
2. l: St*
3. f: St
St
4. s: St
5. s': St
6. f(s') = s
7. u: St
8. v: St*
9. mem_f(St;s';v) 
mem_f(St;s;(+f)(v))
10. u = s'
u = s 
f(u) = s mem_f(St;s;(+f)(v))
By:
RWH (RevHypC 10) 6
THEN
ProveProp
Generated subgoals:None
About:
