PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: shorten list 2 1
1. T: Type
2. L: T*
3. La: T*
4. Fin(T)
5. u: T
6. v: T*
7. La':T*. (t:T. mem_f(T;t;v) mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') mem_f(T;t;v)) & (||La'||1 mem_f(T;hd(La');L))
8. mem_f(T;u;L)

La':T*. (t:T. u = t mem_f(T;t;v) mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') u = t mem_f(T;t;v)) & (||La'||1 mem_f(T;hd(La');L))
By:
Analyze -2
THEN
InstConcl [La']
Generated subgoals:

17. 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')
27. 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)
37. 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)

About:
existslistandallimplies
orequalnatural_numberuniverse