Level: Lib Thy Top:
Hypotheses:None
Conclusion:
St:
. l:St List. s:St. eq:St 
St 
. sx:St.
mem_f(St;sx;l \ s) 
if eq s sx then False else mem_f(St;sx;l) fi
Applied Tactic: (RepD THENM D 0 ...a)
Generated subgoals:1. mem_f(St;sx;l \ s) if eq s sx then False else mem_f(St;sx;l) fi 2. mem_f(St;sx;l \ s) if eq s sx then False else mem_f(St;sx;l) fi