Nuprl - Pf shorten

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

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))

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: Inst Thm* s:S, l:S*. Fin(S) Dec(mem_f(S;s;l)) [T;u;L] THEN Analyze -1

Generated subgoals:

1 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))

2 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))

About:

1	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))`
2	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))`