Level: Lib Thy Top:
Hypotheses:None
Conclusion:
St:
. l:St List. eq:St 
St 
.
(x,y:St. 
(eq x y) 
x = y) (s:St. mem_f(St;s;l) 
mem_f(St;s;LShort(l)))
Applied Tactic: (GenRepD THENM ListInd 2 ...a)
Generated subgoals:1. mem_f(St;s;[]) mem_f(St;s;LShort([]))2. mem_f(St;s;u::v) mem_f(St;s;LShort((u::v)))
3. mem_f(St;s;LShort([])) mem_f(St;s;[])
4. mem_f(St;s;LShort((u::v))) mem_f(St;s;u::v)