At: lshort mem 2 1 2 1 2
1. St: Type
2. l: St*
3. eq: St
St
4. 
x,y:St. eq(x,y) 
x = y
5. s: St
6. u: St
7. v: St*
8. mem_f(St;s;v) mem_f(St;s;LShort(v))
9. mem_f(St;s;v)
10. 
eq(u,s)
u = s 
mem_f(St;s;LShort(v))
By: ProveProp
Generated subgoals:None
About:
