PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: shorten list

T:Type, L,La:T*. Fin(T) (La':T*. (t:T. mem_f(T;t;La) mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') mem_f(T;t;La)) & (||La'||1 mem_f(T;hd(La');L)))
By:
RepD
THEN
ListInd 3
THEN
Reduce 0
Generated subgoals:

11. T: Type
2. L: T*
3. La: T*
4. Fin(T)
La':T*. (t:T. False mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') False) & (||La'||1 mem_f(T;hd(La');L))
21. 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))
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))

About:
alluniverselistimpliesexists
andornatural_numberfalseequal