1 | 7. La': T* 8. t:T. mem_f(T;t;v)  mem_f(T;t;L) mem_f(T;t;La') 9. t:T. mem_f(T;t;La')  mem_f(T;t;v) 10. ||La'|| 1  mem_f(T;hd(La');L) 11. mem_f(T;u;L) 12. t: T 13. u = t mem_f(T;t;v) mem_f(T;t;L) mem_f(T;t;La') |
2 | 7. La': T* 8. t:T. mem_f(T;t;v)  mem_f(T;t;L) mem_f(T;t;La') 9. t:T. mem_f(T;t;La')  mem_f(T;t;v) 10. ||La'|| 1  mem_f(T;hd(La');L) 11. mem_f(T;u;L) 12. t: T 13. mem_f(T;t;La') u = t mem_f(T;t;v) |
3 | 7. La': T* 8. t:T. mem_f(T;t;v)  mem_f(T;t;L) mem_f(T;t;La') 9. t:T. mem_f(T;t;La')  mem_f(T;t;v) 10. ||La'|| 1  mem_f(T;hd(La');L) 11. mem_f(T;u;L) 12. ||La'|| 1 mem_f(T;hd(La');L) |